Step |
Hyp |
Ref |
Expression |
1 |
|
phplem2.1 |
⊢ 𝐴 ∈ V |
2 |
|
phplem2.2 |
⊢ 𝐵 ∈ V |
3 |
|
snex |
⊢ { 〈 𝐵 , 𝐴 〉 } ∈ V |
4 |
2 1
|
f1osn |
⊢ { 〈 𝐵 , 𝐴 〉 } : { 𝐵 } –1-1-onto→ { 𝐴 } |
5 |
|
f1oen3g |
⊢ ( ( { 〈 𝐵 , 𝐴 〉 } ∈ V ∧ { 〈 𝐵 , 𝐴 〉 } : { 𝐵 } –1-1-onto→ { 𝐴 } ) → { 𝐵 } ≈ { 𝐴 } ) |
6 |
3 4 5
|
mp2an |
⊢ { 𝐵 } ≈ { 𝐴 } |
7 |
1
|
difexi |
⊢ ( 𝐴 ∖ { 𝐵 } ) ∈ V |
8 |
7
|
enref |
⊢ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) |
9 |
6 8
|
pm3.2i |
⊢ ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) ) |
10 |
|
incom |
⊢ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) |
11 |
|
difss |
⊢ ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 |
12 |
|
ssrin |
⊢ ( ( 𝐴 ∖ { 𝐵 } ) ⊆ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } ) ) |
13 |
11 12
|
ax-mp |
⊢ ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ( 𝐴 ∩ { 𝐴 } ) |
14 |
|
nnord |
⊢ ( 𝐴 ∈ ω → Ord 𝐴 ) |
15 |
|
orddisj |
⊢ ( Ord 𝐴 → ( 𝐴 ∩ { 𝐴 } ) = ∅ ) |
16 |
14 15
|
syl |
⊢ ( 𝐴 ∈ ω → ( 𝐴 ∩ { 𝐴 } ) = ∅ ) |
17 |
13 16
|
sseqtrid |
⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ ) |
18 |
|
ss0 |
⊢ ( ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) ⊆ ∅ → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ ) |
19 |
17 18
|
syl |
⊢ ( 𝐴 ∈ ω → ( ( 𝐴 ∖ { 𝐵 } ) ∩ { 𝐴 } ) = ∅ ) |
20 |
10 19
|
eqtrid |
⊢ ( 𝐴 ∈ ω → ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) |
21 |
|
disjdif |
⊢ ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ |
22 |
20 21
|
jctil |
⊢ ( 𝐴 ∈ ω → ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) ) |
23 |
|
unen |
⊢ ( ( ( { 𝐵 } ≈ { 𝐴 } ∧ ( 𝐴 ∖ { 𝐵 } ) ≈ ( 𝐴 ∖ { 𝐵 } ) ) ∧ ( ( { 𝐵 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ∧ ( { 𝐴 } ∩ ( 𝐴 ∖ { 𝐵 } ) ) = ∅ ) ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ) |
24 |
9 22 23
|
sylancr |
⊢ ( 𝐴 ∈ ω → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ) |
25 |
24
|
adantr |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ≈ ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) ) |
26 |
|
uncom |
⊢ ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) |
27 |
|
difsnid |
⊢ ( 𝐵 ∈ 𝐴 → ( ( 𝐴 ∖ { 𝐵 } ) ∪ { 𝐵 } ) = 𝐴 ) |
28 |
26 27
|
eqtrid |
⊢ ( 𝐵 ∈ 𝐴 → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 ) |
29 |
28
|
adantl |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐵 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = 𝐴 ) |
30 |
|
phplem1 |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → ( { 𝐴 } ∪ ( 𝐴 ∖ { 𝐵 } ) ) = ( suc 𝐴 ∖ { 𝐵 } ) ) |
31 |
25 29 30
|
3brtr3d |
⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ 𝐴 ) → 𝐴 ≈ ( suc 𝐴 ∖ { 𝐵 } ) ) |