Proof of Theorem sbthfilem
| Step | Hyp | Ref
| Expression |
| 1 | | 19.42vv 1957 |
. . 3
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
| 2 | | 3anass 1095 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ (𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
| 3 | 2 | 2exbii 1849 |
. . 3
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ ∃𝑓∃𝑔(𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
| 4 | | 3anass 1095 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (𝐵 ∈ Fin ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
| 5 | | sbthfilem.4 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
| 6 | 5 | brdom 9001 |
. . . . . . 7
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
| 7 | | sbthfilem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
| 8 | 7 | brdom 9001 |
. . . . . . 7
⊢ (𝐵 ≼ 𝐴 ↔ ∃𝑔 𝑔:𝐵–1-1→𝐴) |
| 9 | 6, 8 | anbi12i 628 |
. . . . . 6
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (∃𝑓 𝑓:𝐴–1-1→𝐵 ∧ ∃𝑔 𝑔:𝐵–1-1→𝐴)) |
| 10 | | exdistrv 1955 |
. . . . . 6
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ (∃𝑓 𝑓:𝐴–1-1→𝐵 ∧ ∃𝑔 𝑔:𝐵–1-1→𝐴)) |
| 11 | 9, 10 | bitr4i 278 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) |
| 12 | 11 | anbi2i 623 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
| 13 | 4, 12 | bitri 275 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
| 14 | 1, 3, 13 | 3bitr4ri 304 |
. 2
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ ∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) |
| 15 | | f1fn 6805 |
. . . . . 6
⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔 Fn 𝐵) |
| 16 | | sbthfilem.3 |
. . . . . . . 8
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
| 17 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
| 18 | 17 | resex 6047 |
. . . . . . . . 9
⊢ (𝑓 ↾ ∪ 𝐷)
∈ V |
| 19 | | fnfi 9218 |
. . . . . . . . . 10
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → 𝑔 ∈ Fin) |
| 20 | | cnvfi 9216 |
. . . . . . . . . 10
⊢ (𝑔 ∈ Fin → ◡𝑔 ∈ Fin) |
| 21 | | resexg 6045 |
. . . . . . . . . 10
⊢ (◡𝑔 ∈ Fin → (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) |
| 22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) |
| 23 | | unexg 7763 |
. . . . . . . . 9
⊢ (((𝑓 ↾ ∪ 𝐷)
∈ V ∧ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) → ((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∈ V) |
| 24 | 18, 22, 23 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∈ V) |
| 25 | 16, 24 | eqeltrid 2845 |
. . . . . . 7
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → 𝐻 ∈ V) |
| 26 | 25 | ancoms 458 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ 𝑔 Fn 𝐵) → 𝐻 ∈ V) |
| 27 | 15, 26 | sylan2 593 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻 ∈ V) |
| 28 | 27 | 3adant2 1132 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻 ∈ V) |
| 29 | | sbthfilem.2 |
. . . . . 6
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
| 30 | 7, 29, 16 | sbthlem9 9131 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |
| 31 | 30 | 3adant1 1131 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |
| 32 | | f1oen3g 9007 |
. . . 4
⊢ ((𝐻 ∈ V ∧ 𝐻:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
| 33 | 28, 31, 32 | syl2anc 584 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐴 ≈ 𝐵) |
| 34 | 33 | exlimivv 1932 |
. 2
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐴 ≈ 𝐵) |
| 35 | 14, 34 | sylbi 217 |
1
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |