Proof of Theorem phplem2
Step | Hyp | Ref
| Expression |
1 | | snex 5140 |
. . . . . 6
⊢
{〈𝐵, 𝐴〉} ∈
V |
2 | | phplem2.2 |
. . . . . . 7
⊢ 𝐵 ∈ V |
3 | | phplem2.1 |
. . . . . . 7
⊢ 𝐴 ∈ V |
4 | 2, 3 | f1osn 6430 |
. . . . . 6
⊢
{〈𝐵, 𝐴〉}:{𝐵}–1-1-onto→{𝐴} |
5 | | f1oen3g 8257 |
. . . . . 6
⊢
(({〈𝐵, 𝐴〉} ∈ V ∧
{〈𝐵, 𝐴〉}:{𝐵}–1-1-onto→{𝐴}) → {𝐵} ≈ {𝐴}) |
6 | 1, 4, 5 | mp2an 682 |
. . . . 5
⊢ {𝐵} ≈ {𝐴} |
7 | 3 | difexi 5046 |
. . . . . 6
⊢ (𝐴 ∖ {𝐵}) ∈ V |
8 | 7 | enref 8274 |
. . . . 5
⊢ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵}) |
9 | 6, 8 | pm3.2i 464 |
. . . 4
⊢ ({𝐵} ≈ {𝐴} ∧ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵})) |
10 | | incom 4028 |
. . . . . 6
⊢ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ((𝐴 ∖ {𝐵}) ∩ {𝐴}) |
11 | | difss 3960 |
. . . . . . . . 9
⊢ (𝐴 ∖ {𝐵}) ⊆ 𝐴 |
12 | | ssrin 4058 |
. . . . . . . . 9
⊢ ((𝐴 ∖ {𝐵}) ⊆ 𝐴 → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ (𝐴 ∩ {𝐴})) |
13 | 11, 12 | ax-mp 5 |
. . . . . . . 8
⊢ ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ (𝐴 ∩ {𝐴}) |
14 | | nnord 7351 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → Ord 𝐴) |
15 | | orddisj 6014 |
. . . . . . . . 9
⊢ (Ord
𝐴 → (𝐴 ∩ {𝐴}) = ∅) |
16 | 14, 15 | syl 17 |
. . . . . . . 8
⊢ (𝐴 ∈ ω → (𝐴 ∩ {𝐴}) = ∅) |
17 | 13, 16 | syl5sseq 3872 |
. . . . . . 7
⊢ (𝐴 ∈ ω → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ ∅) |
18 | | ss0 4200 |
. . . . . . 7
⊢ (((𝐴 ∖ {𝐵}) ∩ {𝐴}) ⊆ ∅ → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) = ∅) |
19 | 17, 18 | syl 17 |
. . . . . 6
⊢ (𝐴 ∈ ω → ((𝐴 ∖ {𝐵}) ∩ {𝐴}) = ∅) |
20 | 10, 19 | syl5eq 2826 |
. . . . 5
⊢ (𝐴 ∈ ω → ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅) |
21 | | disjdif 4264 |
. . . . 5
⊢ ({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ |
22 | 20, 21 | jctil 515 |
. . . 4
⊢ (𝐴 ∈ ω → (({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ ∧ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅)) |
23 | | unen 8328 |
. . . 4
⊢ ((({𝐵} ≈ {𝐴} ∧ (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {𝐵})) ∧ (({𝐵} ∩ (𝐴 ∖ {𝐵})) = ∅ ∧ ({𝐴} ∩ (𝐴 ∖ {𝐵})) = ∅)) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
24 | 9, 22, 23 | sylancr 581 |
. . 3
⊢ (𝐴 ∈ ω → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
25 | 24 | adantr 474 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) ≈ ({𝐴} ∪ (𝐴 ∖ {𝐵}))) |
26 | | uncom 3980 |
. . . 4
⊢ ({𝐵} ∪ (𝐴 ∖ {𝐵})) = ((𝐴 ∖ {𝐵}) ∪ {𝐵}) |
27 | | difsnid 4572 |
. . . 4
⊢ (𝐵 ∈ 𝐴 → ((𝐴 ∖ {𝐵}) ∪ {𝐵}) = 𝐴) |
28 | 26, 27 | syl5eq 2826 |
. . 3
⊢ (𝐵 ∈ 𝐴 → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
29 | 28 | adantl 475 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐵} ∪ (𝐴 ∖ {𝐵})) = 𝐴) |
30 | | phplem1 8427 |
. 2
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → ({𝐴} ∪ (𝐴 ∖ {𝐵})) = (suc 𝐴 ∖ {𝐵})) |
31 | 25, 29, 30 | 3brtr3d 4917 |
1
⊢ ((𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴) → 𝐴 ≈ (suc 𝐴 ∖ {𝐵})) |