Proof of Theorem phplem2
Step | Hyp | Ref
| Expression |
1 | | snex 4908 |
. . . . . 6
⊢
{〈𝐵, 𝐴〉} ∈
V |
2 | | phplem2.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
3 | | phplem2.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
4 | 2, 3 | f1osn 6176 |
. . . . . 6
⊢
{〈𝐵, 𝐴〉}:{𝐵}–1-1-onto→{𝐴} |
5 | | f1oen3g 7971 |
. . . . . 6
⊢
(({〈𝐵, 𝐴〉} ∈ V ∧
{〈𝐵, 𝐴〉}:{𝐵}–1-1-onto→{𝐴}) → {𝐵} ≈ {𝐴}) |
6 | 1, 4, 5 | mp2an 708 |
. . . . 5
⊢ {𝐵} ≈ {𝐴} |
7 | | difss 3737 |
. . . . . . 7
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
8 | 3, 7 | ssexi 4803 |
. . . . . 6
⊢ (𝐴 ∖ {𝐵}) ∈ V |
9 | 8 | enref 7988 |
. . . . 5
⊢ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵}) |
10 | 6, 9 | pm3.2i 471 |
. . . 4
⊢ ({𝐵} ≈ {𝐴} ∧ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵})) |
11 | | incom 3805 |
. . . . . 6
⊢ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ((𝐴 ∖ {𝐵}) ∩ {𝐴}) |
12 | | ssrin 3838 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ (𝐴 ∩ {𝐴})) |
13 | 7, 12 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ (𝐴 ∩ {𝐴}) |
14 | | nnord 7073 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → Ord 𝐴) |
15 | | orddisj 5762 |
. . . . . . . . 9
⊢ (Ord
𝐴 → (𝐴 ∩ {𝐴}) = ∅) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴 ∩ {𝐴}) = ∅) |
17 | 13, 16 | syl5sseq 3653 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ ∅) |
18 | | ss0 3974 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ ∅ → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) = ∅) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) = ∅) |
20 | 11, 19 | syl5eq 2668 |
. . . . 5
⊢ (𝐴 ∈ ω → ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅) |
21 | | disjdif 4040 |
. . . . 5
⊢ ({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ |
22 | 20, 21 | jctil 560 |
. . . 4
⊢ (𝐴 ∈ ω → (({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ ∧ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅)) |
23 | | unen 8040 |
. . . 4
⊢ ((({𝐵} ≈ {𝐴} ∧ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵})) ∧ (({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ ∧ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅)) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
24 | 10, 22, 23 | sylancr 695 |
. . 3
⊢ (𝐴 ∈ ω → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
25 | 24 | adantr 481 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
26 | | uncom 3757 |
. . . 4
⊢ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = ((𝐴 ∖ {𝐵}) ∪ {𝐵}) |
27 | | difsnid 4341 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
28 | 26, 27 | syl5eq 2668 |
. . 3
⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
29 | 28 | adantl 482 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
30 | | phplem1 8139 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) |
31 | 25, 29, 30 | 3brtr3d 4684 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |