| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | brdomi 9000 | . . . 4
⊢ (ω
≼ 𝐴 →
∃𝑓 𝑓:ω–1-1→𝐴) | 
| 2 | 1 | adantr 480 | . . 3
⊢ ((ω
≼ 𝐴 ∧ 𝐵 ∈ 𝐴) → ∃𝑓 𝑓:ω–1-1→𝐴) | 
| 3 |  | reldom 8992 | . . . . . . 7
⊢ Rel
≼ | 
| 4 | 3 | brrelex2i 5741 | . . . . . 6
⊢ (ω
≼ 𝐴 → 𝐴 ∈ V) | 
| 5 | 4 | ad2antrr 726 | . . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝐴 ∈ V) | 
| 6 |  | simplr 768 | . . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝐵 ∈ 𝐴) | 
| 7 |  | f1f 6803 | . . . . . . 7
⊢ (𝑓:ω–1-1→𝐴 → 𝑓:ω⟶𝐴) | 
| 8 | 7 | adantl 481 | . . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝑓:ω⟶𝐴) | 
| 9 |  | peano1 7911 | . . . . . 6
⊢ ∅
∈ ω | 
| 10 |  | ffvelcdm 7100 | . . . . . 6
⊢ ((𝑓:ω⟶𝐴 ∧ ∅ ∈ ω)
→ (𝑓‘∅)
∈ 𝐴) | 
| 11 | 8, 9, 10 | sylancl 586 | . . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓‘∅) ∈ 𝐴) | 
| 12 |  | difsnen 9094 | . . . . 5
⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ 𝐴 ∧ (𝑓‘∅) ∈ 𝐴) → (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {(𝑓‘∅)})) | 
| 13 | 5, 6, 11, 12 | syl3anc 1372 | . . . 4
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {(𝑓‘∅)})) | 
| 14 |  | vex 3483 | . . . . . . . . . 10
⊢ 𝑓 ∈ V | 
| 15 |  | f1f1orn 6858 | . . . . . . . . . . 11
⊢ (𝑓:ω–1-1→𝐴 → 𝑓:ω–1-1-onto→ran
𝑓) | 
| 16 | 15 | adantl 481 | . . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝑓:ω–1-1-onto→ran
𝑓) | 
| 17 |  | f1oen3g 9008 | . . . . . . . . . 10
⊢ ((𝑓 ∈ V ∧ 𝑓:ω–1-1-onto→ran
𝑓) → ω ≈
ran 𝑓) | 
| 18 | 14, 16, 17 | sylancr 587 | . . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ω ≈ ran 𝑓) | 
| 19 | 18 | ensymd 9046 | . . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ran 𝑓 ≈ ω) | 
| 20 | 3 | brrelex1i 5740 | . . . . . . . . . . 11
⊢ (ω
≼ 𝐴 → ω
∈ V) | 
| 21 | 20 | ad2antrr 726 | . . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ω ∈ V) | 
| 22 |  | limom 7904 | . . . . . . . . . . 11
⊢ Lim
ω | 
| 23 | 22 | limenpsi 9193 | . . . . . . . . . 10
⊢ (ω
∈ V → ω ≈ (ω ∖ {∅})) | 
| 24 | 21, 23 | syl 17 | . . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ω ≈ (ω ∖
{∅})) | 
| 25 | 14 | resex 6046 | . . . . . . . . . . 11
⊢ (𝑓 ↾ (ω ∖
{∅})) ∈ V | 
| 26 |  | simpr 484 | . . . . . . . . . . . 12
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝑓:ω–1-1→𝐴) | 
| 27 |  | difss 4135 | . . . . . . . . . . . 12
⊢ (ω
∖ {∅}) ⊆ ω | 
| 28 |  | f1ores 6861 | . . . . . . . . . . . 12
⊢ ((𝑓:ω–1-1→𝐴 ∧ (ω ∖ {∅}) ⊆
ω) → (𝑓 ↾
(ω ∖ {∅})):(ω ∖ {∅})–1-1-onto→(𝑓 “ (ω ∖
{∅}))) | 
| 29 | 26, 27, 28 | sylancl 586 | . . . . . . . . . . 11
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓 ↾ (ω ∖
{∅})):(ω ∖ {∅})–1-1-onto→(𝑓 “ (ω ∖
{∅}))) | 
| 30 |  | f1oen3g 9008 | . . . . . . . . . . 11
⊢ (((𝑓 ↾ (ω ∖
{∅})) ∈ V ∧ (𝑓 ↾ (ω ∖
{∅})):(ω ∖ {∅})–1-1-onto→(𝑓 “ (ω ∖ {∅}))) →
(ω ∖ {∅}) ≈ (𝑓 “ (ω ∖
{∅}))) | 
| 31 | 25, 29, 30 | sylancr 587 | . . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (ω ∖ {∅}) ≈
(𝑓 “ (ω ∖
{∅}))) | 
| 32 |  | f1orn 6857 | . . . . . . . . . . . . 13
⊢ (𝑓:ω–1-1-onto→ran
𝑓 ↔ (𝑓 Fn ω ∧ Fun ◡𝑓)) | 
| 33 | 32 | simprbi 496 | . . . . . . . . . . . 12
⊢ (𝑓:ω–1-1-onto→ran
𝑓 → Fun ◡𝑓) | 
| 34 |  | imadif 6649 | . . . . . . . . . . . 12
⊢ (Fun
◡𝑓 → (𝑓 “ (ω ∖ {∅})) =
((𝑓 “ ω)
∖ (𝑓 “
{∅}))) | 
| 35 | 16, 33, 34 | 3syl 18 | . . . . . . . . . . 11
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓 “ (ω ∖ {∅})) =
((𝑓 “ ω)
∖ (𝑓 “
{∅}))) | 
| 36 |  | f1fn 6804 | . . . . . . . . . . . . . 14
⊢ (𝑓:ω–1-1→𝐴 → 𝑓 Fn ω) | 
| 37 | 36 | adantl 481 | . . . . . . . . . . . . 13
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝑓 Fn ω) | 
| 38 |  | fnima 6697 | . . . . . . . . . . . . 13
⊢ (𝑓 Fn ω → (𝑓 “ ω) = ran 𝑓) | 
| 39 | 37, 38 | syl 17 | . . . . . . . . . . . 12
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓 “ ω) = ran 𝑓) | 
| 40 |  | fnsnfv 6987 | . . . . . . . . . . . . . 14
⊢ ((𝑓 Fn ω ∧ ∅ ∈
ω) → {(𝑓‘∅)} = (𝑓 “ {∅})) | 
| 41 | 37, 9, 40 | sylancl 586 | . . . . . . . . . . . . 13
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → {(𝑓‘∅)} = (𝑓 “ {∅})) | 
| 42 | 41 | eqcomd 2742 | . . . . . . . . . . . 12
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓 “ {∅}) = {(𝑓‘∅)}) | 
| 43 | 39, 42 | difeq12d 4126 | . . . . . . . . . . 11
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((𝑓 “ ω) ∖ (𝑓 “ {∅})) = (ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 44 | 35, 43 | eqtrd 2776 | . . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓 “ (ω ∖ {∅})) = (ran
𝑓 ∖ {(𝑓‘∅)})) | 
| 45 | 31, 44 | breqtrd 5168 | . . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (ω ∖ {∅}) ≈
(ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 46 |  | entr 9047 | . . . . . . . . 9
⊢ ((ω
≈ (ω ∖ {∅}) ∧ (ω ∖ {∅}) ≈
(ran 𝑓 ∖ {(𝑓‘∅)})) →
ω ≈ (ran 𝑓
∖ {(𝑓‘∅)})) | 
| 47 | 24, 45, 46 | syl2anc 584 | . . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ω ≈ (ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 48 |  | entr 9047 | . . . . . . . 8
⊢ ((ran
𝑓 ≈ ω ∧
ω ≈ (ran 𝑓
∖ {(𝑓‘∅)})) → ran 𝑓 ≈ (ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 49 | 19, 47, 48 | syl2anc 584 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ran 𝑓 ≈ (ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 50 |  | difexg 5328 | . . . . . . . 8
⊢ (𝐴 ∈ V → (𝐴 ∖ ran 𝑓) ∈ V) | 
| 51 |  | enrefg 9025 | . . . . . . . 8
⊢ ((𝐴 ∖ ran 𝑓) ∈ V → (𝐴 ∖ ran 𝑓) ≈ (𝐴 ∖ ran 𝑓)) | 
| 52 | 5, 50, 51 | 3syl 18 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝐴 ∖ ran 𝑓) ≈ (𝐴 ∖ ran 𝑓)) | 
| 53 |  | disjdif 4471 | . . . . . . . 8
⊢ (ran
𝑓 ∩ (𝐴 ∖ ran 𝑓)) = ∅ | 
| 54 | 53 | a1i 11 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (ran 𝑓 ∩ (𝐴 ∖ ran 𝑓)) = ∅) | 
| 55 |  | difss 4135 | . . . . . . . . . 10
⊢ (ran
𝑓 ∖ {(𝑓‘∅)}) ⊆ ran
𝑓 | 
| 56 |  | ssrin 4241 | . . . . . . . . . 10
⊢ ((ran
𝑓 ∖ {(𝑓‘∅)}) ⊆ ran
𝑓 → ((ran 𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) ⊆ (ran 𝑓 ∩ (𝐴 ∖ ran 𝑓))) | 
| 57 | 55, 56 | ax-mp 5 | . . . . . . . . 9
⊢ ((ran
𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) ⊆ (ran 𝑓 ∩ (𝐴 ∖ ran 𝑓)) | 
| 58 |  | sseq0 4402 | . . . . . . . . 9
⊢ ((((ran
𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) ⊆ (ran 𝑓 ∩ (𝐴 ∖ ran 𝑓)) ∧ (ran 𝑓 ∩ (𝐴 ∖ ran 𝑓)) = ∅) → ((ran 𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) = ∅) | 
| 59 | 57, 53, 58 | mp2an 692 | . . . . . . . 8
⊢ ((ran
𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) = ∅ | 
| 60 | 59 | a1i 11 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((ran 𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) = ∅) | 
| 61 |  | unen 9087 | . . . . . . 7
⊢ (((ran
𝑓 ≈ (ran 𝑓 ∖ {(𝑓‘∅)}) ∧ (𝐴 ∖ ran 𝑓) ≈ (𝐴 ∖ ran 𝑓)) ∧ ((ran 𝑓 ∩ (𝐴 ∖ ran 𝑓)) = ∅ ∧ ((ran 𝑓 ∖ {(𝑓‘∅)}) ∩ (𝐴 ∖ ran 𝑓)) = ∅)) → (ran 𝑓 ∪ (𝐴 ∖ ran 𝑓)) ≈ ((ran 𝑓 ∖ {(𝑓‘∅)}) ∪ (𝐴 ∖ ran 𝑓))) | 
| 62 | 49, 52, 54, 60, 61 | syl22anc 838 | . . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (ran 𝑓 ∪ (𝐴 ∖ ran 𝑓)) ≈ ((ran 𝑓 ∖ {(𝑓‘∅)}) ∪ (𝐴 ∖ ran 𝑓))) | 
| 63 | 8 | frnd 6743 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ran 𝑓 ⊆ 𝐴) | 
| 64 |  | undif 4481 | . . . . . . 7
⊢ (ran
𝑓 ⊆ 𝐴 ↔ (ran 𝑓 ∪ (𝐴 ∖ ran 𝑓)) = 𝐴) | 
| 65 | 63, 64 | sylib 218 | . . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (ran 𝑓 ∪ (𝐴 ∖ ran 𝑓)) = 𝐴) | 
| 66 |  | uncom 4157 | . . . . . . 7
⊢ ((ran
𝑓 ∖ {(𝑓‘∅)}) ∪ (𝐴 ∖ ran 𝑓)) = ((𝐴 ∖ ran 𝑓) ∪ (ran 𝑓 ∖ {(𝑓‘∅)})) | 
| 67 |  | eldifn 4131 | . . . . . . . . . . 11
⊢ ((𝑓‘∅) ∈ (𝐴 ∖ ran 𝑓) → ¬ (𝑓‘∅) ∈ ran 𝑓) | 
| 68 |  | fnfvelrn 7099 | . . . . . . . . . . . 12
⊢ ((𝑓 Fn ω ∧ ∅ ∈
ω) → (𝑓‘∅) ∈ ran 𝑓) | 
| 69 | 37, 9, 68 | sylancl 586 | . . . . . . . . . . 11
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝑓‘∅) ∈ ran 𝑓) | 
| 70 | 67, 69 | nsyl3 138 | . . . . . . . . . 10
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ¬ (𝑓‘∅) ∈ (𝐴 ∖ ran 𝑓)) | 
| 71 |  | disjsn 4710 | . . . . . . . . . 10
⊢ (((𝐴 ∖ ran 𝑓) ∩ {(𝑓‘∅)}) = ∅ ↔ ¬
(𝑓‘∅) ∈
(𝐴 ∖ ran 𝑓)) | 
| 72 | 70, 71 | sylibr 234 | . . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((𝐴 ∖ ran 𝑓) ∩ {(𝑓‘∅)}) = ∅) | 
| 73 |  | undif4 4466 | . . . . . . . . 9
⊢ (((𝐴 ∖ ran 𝑓) ∩ {(𝑓‘∅)}) = ∅ → ((𝐴 ∖ ran 𝑓) ∪ (ran 𝑓 ∖ {(𝑓‘∅)})) = (((𝐴 ∖ ran 𝑓) ∪ ran 𝑓) ∖ {(𝑓‘∅)})) | 
| 74 | 72, 73 | syl 17 | . . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((𝐴 ∖ ran 𝑓) ∪ (ran 𝑓 ∖ {(𝑓‘∅)})) = (((𝐴 ∖ ran 𝑓) ∪ ran 𝑓) ∖ {(𝑓‘∅)})) | 
| 75 |  | uncom 4157 | . . . . . . . . . 10
⊢ ((𝐴 ∖ ran 𝑓) ∪ ran 𝑓) = (ran 𝑓 ∪ (𝐴 ∖ ran 𝑓)) | 
| 76 | 75, 65 | eqtrid 2788 | . . . . . . . . 9
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((𝐴 ∖ ran 𝑓) ∪ ran 𝑓) = 𝐴) | 
| 77 | 76 | difeq1d 4124 | . . . . . . . 8
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (((𝐴 ∖ ran 𝑓) ∪ ran 𝑓) ∖ {(𝑓‘∅)}) = (𝐴 ∖ {(𝑓‘∅)})) | 
| 78 | 74, 77 | eqtrd 2776 | . . . . . . 7
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((𝐴 ∖ ran 𝑓) ∪ (ran 𝑓 ∖ {(𝑓‘∅)})) = (𝐴 ∖ {(𝑓‘∅)})) | 
| 79 | 66, 78 | eqtrid 2788 | . . . . . 6
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → ((ran 𝑓 ∖ {(𝑓‘∅)}) ∪ (𝐴 ∖ ran 𝑓)) = (𝐴 ∖ {(𝑓‘∅)})) | 
| 80 | 62, 65, 79 | 3brtr3d 5173 | . . . . 5
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → 𝐴 ≈ (𝐴 ∖ {(𝑓‘∅)})) | 
| 81 | 80 | ensymd 9046 | . . . 4
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝐴 ∖ {(𝑓‘∅)}) ≈ 𝐴) | 
| 82 |  | entr 9047 | . . . 4
⊢ (((𝐴 ∖ {𝐵}) ≈ (𝐴 ∖ {(𝑓‘∅)}) ∧ (𝐴 ∖ {(𝑓‘∅)}) ≈ 𝐴) → (𝐴 ∖ {𝐵}) ≈ 𝐴) | 
| 83 | 13, 81, 82 | syl2anc 584 | . . 3
⊢
(((ω ≼ 𝐴
∧ 𝐵 ∈ 𝐴) ∧ 𝑓:ω–1-1→𝐴) → (𝐴 ∖ {𝐵}) ≈ 𝐴) | 
| 84 | 2, 83 | exlimddv 1934 | . 2
⊢ ((ω
≼ 𝐴 ∧ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ≈ 𝐴) | 
| 85 |  | difsn 4797 | . . . 4
⊢ (¬
𝐵 ∈ 𝐴 → (𝐴 ∖ {𝐵}) = 𝐴) | 
| 86 | 85 | adantl 481 | . . 3
⊢ ((ω
≼ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) = 𝐴) | 
| 87 |  | enrefg 9025 | . . . . 5
⊢ (𝐴 ∈ V → 𝐴 ≈ 𝐴) | 
| 88 | 4, 87 | syl 17 | . . . 4
⊢ (ω
≼ 𝐴 → 𝐴 ≈ 𝐴) | 
| 89 | 88 | adantr 480 | . . 3
⊢ ((ω
≼ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → 𝐴 ≈ 𝐴) | 
| 90 | 86, 89 | eqbrtrd 5164 | . 2
⊢ ((ω
≼ 𝐴 ∧ ¬ 𝐵 ∈ 𝐴) → (𝐴 ∖ {𝐵}) ≈ 𝐴) | 
| 91 | 84, 90 | pm2.61dan 812 | 1
⊢ (ω
≼ 𝐴 → (𝐴 ∖ {𝐵}) ≈ 𝐴) |