Proof of Theorem noextendseq
Step | Hyp | Ref
| Expression |
1 | | nofun 31802 |
. . . 4
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | noextend.1 |
. . . . . 6
⊢ 𝑋 ∈ {1𝑜,
2𝑜} |
3 | | fnconstg 6093 |
. . . . . 6
⊢ (𝑋 ∈ {1𝑜,
2𝑜} → ((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴)) |
4 | | fnfun 5988 |
. . . . . 6
⊢ (((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴) → Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) |
5 | 2, 3, 4 | mp2b 10 |
. . . . 5
⊢ Fun
((𝐵 ∖ dom 𝐴) × {𝑋}) |
6 | | snnzg 4308 |
. . . . . . . . 9
⊢ (𝑋 ∈ {1𝑜,
2𝑜} → {𝑋} ≠ ∅) |
7 | | dmxp 5344 |
. . . . . . . . 9
⊢ ({𝑋} ≠ ∅ → dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴)) |
8 | 2, 6, 7 | mp2b 10 |
. . . . . . . 8
⊢ dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴) |
9 | 8 | ineq2i 3811 |
. . . . . . 7
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴)) |
10 | | disjdif 4040 |
. . . . . . 7
⊢ (dom
𝐴 ∩ (𝐵 ∖ dom 𝐴)) = ∅ |
11 | 9, 10 | eqtri 2644 |
. . . . . 6
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅ |
12 | | funun 5932 |
. . . . . 6
⊢ (((Fun
𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
13 | 11, 12 | mpan2 707 |
. . . . 5
⊢ ((Fun
𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
14 | 5, 13 | mpan2 707 |
. . . 4
⊢ (Fun
𝐴 → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
15 | 1, 14 | syl 17 |
. . 3
⊢ (𝐴 ∈
No → Fun (𝐴
∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
16 | 15 | adantr 481 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋}))) |
17 | | dmun 5331 |
. . . 4
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) |
18 | 8 | uneq2i 3764 |
. . . 4
⊢ (dom
𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
19 | 17, 18 | eqtri 2644 |
. . 3
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
20 | | nodmon 31803 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
21 | | undif 4049 |
. . . . . 6
⊢ (dom
𝐴 ⊆ 𝐵 ↔ (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵) |
22 | | eleq1a 2696 |
. . . . . . 7
⊢ (𝐵 ∈ On → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
23 | 22 | adantl 482 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
24 | 21, 23 | syl5bi 232 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
25 | | ssdif0 3942 |
. . . . . 6
⊢ (𝐵 ⊆ dom 𝐴 ↔ (𝐵 ∖ dom 𝐴) = ∅) |
26 | | uneq2 3761 |
. . . . . . . . . 10
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = (dom 𝐴 ∪ ∅)) |
27 | | un0 3967 |
. . . . . . . . . 10
⊢ (dom
𝐴 ∪ ∅) = dom
𝐴 |
28 | 26, 27 | syl6eq 2672 |
. . . . . . . . 9
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = dom 𝐴) |
29 | 28 | eleq1d 2686 |
. . . . . . . 8
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On ↔ dom 𝐴 ∈ On)) |
30 | 29 | biimprcd 240 |
. . . . . . 7
⊢ (dom
𝐴 ∈ On → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
31 | 30 | adantr 481 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
32 | 25, 31 | syl5bi 232 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ dom 𝐴 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
33 | | eloni 5733 |
. . . . . 6
⊢ (dom
𝐴 ∈ On → Ord dom
𝐴) |
34 | | eloni 5733 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
35 | | ordtri2or2 5823 |
. . . . . 6
⊢ ((Ord dom
𝐴 ∧ Ord 𝐵) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
36 | 33, 34, 35 | syl2an 494 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
37 | 24, 32, 36 | mpjaod 396 |
. . . 4
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On) |
38 | 20, 37 | sylan 488 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (dom 𝐴 ∪
(𝐵 ∖ dom 𝐴)) ∈ On) |
39 | 19, 38 | syl5eqel 2705 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → dom (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On) |
40 | | rnun 5541 |
. . 3
⊢ ran
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) |
41 | | norn 31804 |
. . . . 5
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1𝑜, 2𝑜}) |
42 | 41 | adantr 481 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran 𝐴 ⊆
{1𝑜, 2𝑜}) |
43 | | rnxpss 5566 |
. . . . 5
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {𝑋} |
44 | | snssi 4339 |
. . . . . 6
⊢ (𝑋 ∈ {1𝑜,
2𝑜} → {𝑋} ⊆ {1𝑜,
2𝑜}) |
45 | 2, 44 | ax-mp 5 |
. . . . 5
⊢ {𝑋} ⊆
{1𝑜, 2𝑜} |
46 | 43, 45 | sstri 3612 |
. . . 4
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1𝑜,
2𝑜} |
47 | | unss 3787 |
. . . 4
⊢ ((ran
𝐴 ⊆
{1𝑜, 2𝑜} ∧ ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1𝑜,
2𝑜}) ↔ (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1𝑜,
2𝑜}) |
48 | 42, 46, 47 | sylanblc 696 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (ran 𝐴 ∪ ran
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1𝑜,
2𝑜}) |
49 | 40, 48 | syl5eqss 3649 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1𝑜,
2𝑜}) |
50 | | elno2 31807 |
. 2
⊢ ((𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
↔ (Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On ∧ ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1𝑜,
2𝑜})) |
51 | 16, 39, 49, 50 | syl3anbrc 1246 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
) |