Proof of Theorem noextendseq
Step | Hyp | Ref
| Expression |
1 | | nofun 33589 |
. . . 4
⊢ (𝐴 ∈
No → Fun 𝐴) |
2 | | noextend.1 |
. . . . 5
⊢ 𝑋 ∈ {1o,
2o} |
3 | | fnconstg 6607 |
. . . . 5
⊢ (𝑋 ∈ {1o,
2o} → ((𝐵
∖ dom 𝐴) ×
{𝑋}) Fn (𝐵 ∖ dom 𝐴)) |
4 | | fnfun 6479 |
. . . . 5
⊢ (((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴) → Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) |
5 | 2, 3, 4 | mp2b 10 |
. . . 4
⊢ Fun
((𝐵 ∖ dom 𝐴) × {𝑋}) |
6 | | snnzg 4690 |
. . . . . . . 8
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
≠ ∅) |
7 | | dmxp 5798 |
. . . . . . . 8
⊢ ({𝑋} ≠ ∅ → dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴)) |
8 | 2, 6, 7 | mp2b 10 |
. . . . . . 7
⊢ dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴) |
9 | 8 | ineq2i 4124 |
. . . . . 6
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴)) |
10 | | disjdif 4386 |
. . . . . 6
⊢ (dom
𝐴 ∩ (𝐵 ∖ dom 𝐴)) = ∅ |
11 | 9, 10 | eqtri 2765 |
. . . . 5
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅ |
12 | | funun 6426 |
. . . . 5
⊢ (((Fun
𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ (dom 𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
13 | 11, 12 | mpan2 691 |
. . . 4
⊢ ((Fun
𝐴 ∧ Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) → Fun (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
14 | 1, 5, 13 | sylancl 589 |
. . 3
⊢ (𝐴 ∈
No → Fun (𝐴
∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
15 | 14 | adantr 484 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋}))) |
16 | | dmun 5779 |
. . . 4
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) |
17 | 8 | uneq2i 4074 |
. . . 4
⊢ (dom
𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
18 | 16, 17 | eqtri 2765 |
. . 3
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
19 | | nodmon 33590 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
20 | | undif 4396 |
. . . . . 6
⊢ (dom
𝐴 ⊆ 𝐵 ↔ (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵) |
21 | | eleq1a 2833 |
. . . . . . 7
⊢ (𝐵 ∈ On → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
22 | 21 | adantl 485 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
23 | 20, 22 | syl5bi 245 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
24 | | ssdif0 4278 |
. . . . . 6
⊢ (𝐵 ⊆ dom 𝐴 ↔ (𝐵 ∖ dom 𝐴) = ∅) |
25 | | uneq2 4071 |
. . . . . . . . . 10
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = (dom 𝐴 ∪ ∅)) |
26 | | un0 4305 |
. . . . . . . . . 10
⊢ (dom
𝐴 ∪ ∅) = dom
𝐴 |
27 | 25, 26 | eqtrdi 2794 |
. . . . . . . . 9
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = dom 𝐴) |
28 | 27 | eleq1d 2822 |
. . . . . . . 8
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On ↔ dom 𝐴 ∈ On)) |
29 | 28 | biimprcd 253 |
. . . . . . 7
⊢ (dom
𝐴 ∈ On → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
30 | 29 | adantr 484 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
31 | 24, 30 | syl5bi 245 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ dom 𝐴 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
32 | | eloni 6223 |
. . . . . 6
⊢ (dom
𝐴 ∈ On → Ord dom
𝐴) |
33 | | eloni 6223 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
34 | | ordtri2or2 6309 |
. . . . . 6
⊢ ((Ord dom
𝐴 ∧ Ord 𝐵) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
35 | 32, 33, 34 | syl2an 599 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
36 | 23, 31, 35 | mpjaod 860 |
. . . 4
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On) |
37 | 19, 36 | sylan 583 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (dom 𝐴 ∪
(𝐵 ∖ dom 𝐴)) ∈ On) |
38 | 18, 37 | eqeltrid 2842 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → dom (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On) |
39 | | rnun 6009 |
. . 3
⊢ ran
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) |
40 | | norn 33591 |
. . . . 5
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1o, 2o}) |
41 | 40 | adantr 484 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran 𝐴 ⊆
{1o, 2o}) |
42 | | rnxpss 6035 |
. . . . 5
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {𝑋} |
43 | | snssi 4721 |
. . . . . 6
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
⊆ {1o, 2o}) |
44 | 2, 43 | ax-mp 5 |
. . . . 5
⊢ {𝑋} ⊆ {1o,
2o} |
45 | 42, 44 | sstri 3910 |
. . . 4
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o,
2o} |
46 | | unss 4098 |
. . . 4
⊢ ((ran
𝐴 ⊆ {1o,
2o} ∧ ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o, 2o})
↔ (ran 𝐴 ∪ ran
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
47 | 41, 45, 46 | sylanblc 592 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (ran 𝐴 ∪ ran
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
48 | 39, 47 | eqsstrid 3949 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
49 | | elno2 33594 |
. 2
⊢ ((𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
↔ (Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On ∧ ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o})) |
50 | 15, 38, 48, 49 | syl3anbrc 1345 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
) |