Proof of Theorem noextendseq
| Step | Hyp | Ref
| Expression |
| 1 | | nofun 27694 |
. . . 4
⊢ (𝐴 ∈
No → Fun 𝐴) |
| 2 | | noextend.1 |
. . . . 5
⊢ 𝑋 ∈ {1o,
2o} |
| 3 | | fnconstg 6796 |
. . . . 5
⊢ (𝑋 ∈ {1o,
2o} → ((𝐵
∖ dom 𝐴) ×
{𝑋}) Fn (𝐵 ∖ dom 𝐴)) |
| 4 | | fnfun 6668 |
. . . . 5
⊢ (((𝐵 ∖ dom 𝐴) × {𝑋}) Fn (𝐵 ∖ dom 𝐴) → Fun ((𝐵 ∖ dom 𝐴) × {𝑋})) |
| 5 | 2, 3, 4 | mp2b 10 |
. . . 4
⊢ Fun
((𝐵 ∖ dom 𝐴) × {𝑋}) |
| 6 | | snnzg 4774 |
. . . . . . . 8
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
≠ ∅) |
| 7 | | dmxp 5939 |
. . . . . . . 8
⊢ ({𝑋} ≠ ∅ → dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴)) |
| 8 | 2, 6, 7 | mp2b 10 |
. . . . . . 7
⊢ dom
((𝐵 ∖ dom 𝐴) × {𝑋}) = (𝐵 ∖ dom 𝐴) |
| 9 | 8 | ineq2i 4217 |
. . . . . 6
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∩ (𝐵 ∖ dom 𝐴)) |
| 10 | | disjdif 4472 |
. . . . . 6
⊢ (dom
𝐴 ∩ (𝐵 ∖ dom 𝐴)) = ∅ |
| 11 | 9, 10 | eqtri 2765 |
. . . . 5
⊢ (dom
𝐴 ∩ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = ∅ |
| 12 | | funun 6612 |
. . . . 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 586 |
. . 3
⊢ (𝐴 ∈
No → Fun (𝐴
∪ ((𝐵 ∖ dom 𝐴) × {𝑋}))) |
| 15 | 14 | adantr 480 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋}))) |
| 16 | | dmun 5921 |
. . . 4
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) |
| 17 | 8 | uneq2i 4165 |
. . . 4
⊢ (dom
𝐴 ∪ dom ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
| 18 | 16, 17 | eqtri 2765 |
. . 3
⊢ dom
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) |
| 19 | | nodmon 27695 |
. . . 4
⊢ (𝐴 ∈
No → dom 𝐴
∈ On) |
| 20 | | undif 4482 |
. . . . . 6
⊢ (dom
𝐴 ⊆ 𝐵 ↔ (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵) |
| 21 | | eleq1a 2836 |
. . . . . . 7
⊢ (𝐵 ∈ On → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 22 | 21 | adantl 481 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 23 | 20, 22 | biimtrid 242 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 24 | | ssdif0 4366 |
. . . . . 6
⊢ (𝐵 ⊆ dom 𝐴 ↔ (𝐵 ∖ dom 𝐴) = ∅) |
| 25 | | uneq2 4162 |
. . . . . . . . . 10
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = (dom 𝐴 ∪ ∅)) |
| 26 | | un0 4394 |
. . . . . . . . . 10
⊢ (dom
𝐴 ∪ ∅) = dom
𝐴 |
| 27 | 25, 26 | eqtrdi 2793 |
. . . . . . . . 9
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) = dom 𝐴) |
| 28 | 27 | eleq1d 2826 |
. . . . . . . 8
⊢ ((𝐵 ∖ dom 𝐴) = ∅ → ((dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On ↔ dom 𝐴 ∈ On)) |
| 29 | 28 | biimprcd 250 |
. . . . . . 7
⊢ (dom
𝐴 ∈ On → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 30 | 29 | adantr 480 |
. . . . . 6
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐵 ∖ dom 𝐴) = ∅ → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 31 | 24, 30 | biimtrid 242 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 ⊆ dom 𝐴 → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On)) |
| 32 | | eloni 6394 |
. . . . . 6
⊢ (dom
𝐴 ∈ On → Ord dom
𝐴) |
| 33 | | eloni 6394 |
. . . . . 6
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 34 | | ordtri2or2 6483 |
. . . . . 6
⊢ ((Ord dom
𝐴 ∧ Ord 𝐵) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
| 35 | 32, 33, 34 | syl2an 596 |
. . . . 5
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ⊆ 𝐵 ∨ 𝐵 ⊆ dom 𝐴)) |
| 36 | 23, 31, 35 | mpjaod 861 |
. . . 4
⊢ ((dom
𝐴 ∈ On ∧ 𝐵 ∈ On) → (dom 𝐴 ∪ (𝐵 ∖ dom 𝐴)) ∈ On) |
| 37 | 19, 36 | sylan 580 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (dom 𝐴 ∪
(𝐵 ∖ dom 𝐴)) ∈ On) |
| 38 | 18, 37 | eqeltrid 2845 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → dom (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On) |
| 39 | | rnun 6165 |
. . 3
⊢ ran
(𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) = (ran 𝐴 ∪ ran ((𝐵 ∖ dom 𝐴) × {𝑋})) |
| 40 | | norn 27696 |
. . . . 5
⊢ (𝐴 ∈
No → ran 𝐴
⊆ {1o, 2o}) |
| 41 | 40 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran 𝐴 ⊆
{1o, 2o}) |
| 42 | | rnxpss 6192 |
. . . . 5
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {𝑋} |
| 43 | | snssi 4808 |
. . . . . 6
⊢ (𝑋 ∈ {1o,
2o} → {𝑋}
⊆ {1o, 2o}) |
| 44 | 2, 43 | ax-mp 5 |
. . . . 5
⊢ {𝑋} ⊆ {1o,
2o} |
| 45 | 42, 44 | sstri 3993 |
. . . 4
⊢ ran
((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o,
2o} |
| 46 | | unss 4190 |
. . . 4
⊢ ((ran
𝐴 ⊆ {1o,
2o} ∧ ran ((𝐵 ∖ dom 𝐴) × {𝑋}) ⊆ {1o, 2o})
↔ (ran 𝐴 ∪ ran
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
| 47 | 41, 45, 46 | sylanblc 589 |
. . 3
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (ran 𝐴 ∪ ran
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
| 48 | 39, 47 | eqsstrid 4022 |
. 2
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → ran (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o}) |
| 49 | | elno2 27699 |
. 2
⊢ ((𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
↔ (Fun (𝐴 ∪
((𝐵 ∖ dom 𝐴) × {𝑋})) ∧ dom (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ On ∧ ran (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ⊆ {1o,
2o})) |
| 50 | 15, 38, 48, 49 | syl3anbrc 1344 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
On) → (𝐴 ∪ ((𝐵 ∖ dom 𝐴) × {𝑋})) ∈ No
) |