Proof of Theorem sbthfilem
Step | Hyp | Ref
| Expression |
1 | | 19.42vv 1961 |
. . 3
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
2 | | 3anass 1094 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ (𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
3 | 2 | 2exbii 1851 |
. . 3
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ ∃𝑓∃𝑔(𝐵 ∈ Fin ∧ (𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
4 | | 3anass 1094 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (𝐵 ∈ Fin ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴))) |
5 | | sbthfilem.4 |
. . . . . . . 8
⊢ 𝐵 ∈ V |
6 | 5 | brdom 8739 |
. . . . . . 7
⊢ (𝐴 ≼ 𝐵 ↔ ∃𝑓 𝑓:𝐴–1-1→𝐵) |
7 | | sbthfilem.1 |
. . . . . . . 8
⊢ 𝐴 ∈ V |
8 | 7 | brdom 8739 |
. . . . . . 7
⊢ (𝐵 ≼ 𝐴 ↔ ∃𝑔 𝑔:𝐵–1-1→𝐴) |
9 | 6, 8 | anbi12i 627 |
. . . . . 6
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (∃𝑓 𝑓:𝐴–1-1→𝐵 ∧ ∃𝑔 𝑔:𝐵–1-1→𝐴)) |
10 | | exdistrv 1959 |
. . . . . 6
⊢
(∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) ↔ (∃𝑓 𝑓:𝐴–1-1→𝐵 ∧ ∃𝑔 𝑔:𝐵–1-1→𝐴)) |
11 | 9, 10 | bitr4i 277 |
. . . . 5
⊢ ((𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) |
12 | 11 | anbi2i 623 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ (𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴)) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
13 | 4, 12 | bitri 274 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ (𝐵 ∈ Fin ∧ ∃𝑓∃𝑔(𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴))) |
14 | 1, 3, 13 | 3bitr4ri 304 |
. 2
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) ↔ ∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴)) |
15 | | f1fn 6665 |
. . . . . 6
⊢ (𝑔:𝐵–1-1→𝐴 → 𝑔 Fn 𝐵) |
16 | | sbthfilem.3 |
. . . . . . . 8
⊢ 𝐻 = ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) |
17 | | vex 3435 |
. . . . . . . . . 10
⊢ 𝑓 ∈ V |
18 | 17 | resex 5934 |
. . . . . . . . 9
⊢ (𝑓 ↾ ∪ 𝐷)
∈ V |
19 | | fnfi 8953 |
. . . . . . . . . 10
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → 𝑔 ∈ Fin) |
20 | | cnvfi 8952 |
. . . . . . . . . 10
⊢ (𝑔 ∈ Fin → ◡𝑔 ∈ Fin) |
21 | | resexg 5932 |
. . . . . . . . . 10
⊢ (◡𝑔 ∈ Fin → (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) |
22 | 19, 20, 21 | 3syl 18 |
. . . . . . . . 9
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) |
23 | | unexg 7591 |
. . . . . . . . 9
⊢ (((𝑓 ↾ ∪ 𝐷)
∈ V ∧ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷)) ∈ V) → ((𝑓 ↾ ∪ 𝐷)
∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∈ V) |
24 | 18, 22, 23 | sylancr 587 |
. . . . . . . 8
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → ((𝑓 ↾ ∪ 𝐷) ∪ (◡𝑔 ↾ (𝐴 ∖ ∪ 𝐷))) ∈ V) |
25 | 16, 24 | eqeltrid 2843 |
. . . . . . 7
⊢ ((𝑔 Fn 𝐵 ∧ 𝐵 ∈ Fin) → 𝐻 ∈ V) |
26 | 25 | ancoms 459 |
. . . . . 6
⊢ ((𝐵 ∈ Fin ∧ 𝑔 Fn 𝐵) → 𝐻 ∈ V) |
27 | 15, 26 | sylan2 593 |
. . . . 5
⊢ ((𝐵 ∈ Fin ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻 ∈ V) |
28 | 27 | 3adant2 1130 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻 ∈ V) |
29 | | sbthfilem.2 |
. . . . . 6
⊢ 𝐷 = {𝑥 ∣ (𝑥 ⊆ 𝐴 ∧ (𝑔 “ (𝐵 ∖ (𝑓 “ 𝑥))) ⊆ (𝐴 ∖ 𝑥))} |
30 | 7, 29, 16 | sbthlem9 8867 |
. . . . 5
⊢ ((𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |
31 | 30 | 3adant1 1129 |
. . . 4
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐻:𝐴–1-1-onto→𝐵) |
32 | | f1oen3g 8743 |
. . . 4
⊢ ((𝐻 ∈ V ∧ 𝐻:𝐴–1-1-onto→𝐵) → 𝐴 ≈ 𝐵) |
33 | 28, 31, 32 | syl2anc 584 |
. . 3
⊢ ((𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐴 ≈ 𝐵) |
34 | 33 | exlimivv 1935 |
. 2
⊢
(∃𝑓∃𝑔(𝐵 ∈ Fin ∧ 𝑓:𝐴–1-1→𝐵 ∧ 𝑔:𝐵–1-1→𝐴) → 𝐴 ≈ 𝐵) |
35 | 14, 34 | sylbi 216 |
1
⊢ ((𝐵 ∈ Fin ∧ 𝐴 ≼ 𝐵 ∧ 𝐵 ≼ 𝐴) → 𝐴 ≈ 𝐵) |