Step | Hyp | Ref
| Expression |
1 | | ensym 7891 |
. . 3
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
2 | | bren 7850 |
. . 3
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
3 | 1, 2 | sylib 207 |
. 2
⊢ (𝐴 ≈ 𝐵 → ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
4 | | elpwi 4117 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵) |
5 | | simplr 788 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐴 ∈ FinIa) |
6 | | imassrn 5396 |
. . . . . . . . . 10
⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓 |
7 | | f1of 6050 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵⟶𝐴) |
8 | 7 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵⟶𝐴) |
9 | | frn 5966 |
. . . . . . . . . . 11
⊢ (𝑓:𝐵⟶𝐴 → ran 𝑓 ⊆ 𝐴) |
10 | 8, 9 | syl 17 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ran 𝑓 ⊆ 𝐴) |
11 | 6, 10 | syl5ss 3579 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ⊆ 𝐴) |
12 | | fin1ai 8998 |
. . . . . . . . 9
⊢ ((𝐴 ∈ FinIa ∧
(𝑓 “ 𝑥) ⊆ 𝐴) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
13 | 5, 11, 12 | syl2anc 691 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
14 | | f1of1 6049 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
15 | 14 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵–1-1→𝐴) |
16 | | simpr 476 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) |
17 | | vex 3176 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
18 | 17 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ V) |
19 | | f1imaeng 7902 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑥) ≈ 𝑥) |
20 | 15, 16, 18, 19 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
21 | | enfi 8061 |
. . . . . . . . . 10
⊢ ((𝑓 “ 𝑥) ≈ 𝑥 → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
22 | 20, 21 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
23 | | df-f1 5809 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ Fun ◡𝑓)) |
24 | 23 | simprbi 479 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1→𝐴 → Fun ◡𝑓) |
25 | | imadif 5887 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝑓 → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
26 | 15, 24, 25 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
27 | | f1ofo 6057 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–onto→𝐴) |
28 | | foima 6033 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
30 | 29 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
31 | 30 | difeq1d 3689 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
32 | 26, 31 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
33 | | difssd 3700 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ⊆ 𝐵) |
34 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
35 | 7 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝑓:𝐵⟶𝐴) |
36 | | dmfex 7017 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ V) |
37 | 34, 35, 36 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈ V) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐵 ∈ V) |
39 | | difexg 4735 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ V → (𝐵 ∖ 𝑥) ∈ V) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ∈ V) |
41 | | f1imaeng 7902 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝐵 ∖ 𝑥) ⊆ 𝐵 ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
42 | 15, 33, 40, 41 | syl3anc 1318 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
43 | 32, 42 | eqbrtrrd 4607 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
44 | | enfi 8061 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
45 | 43, 44 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
46 | 22, 45 | orbi12d 742 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin) ↔ (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
47 | 13, 46 | mpbid 221 |
. . . . . . 7
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
48 | 4, 47 | sylan2 490 |
. . . . . 6
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
49 | 48 | ralrimiva 2949 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) →
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
50 | | isfin1a 8997 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
51 | 37, 50 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
52 | 49, 51 | mpbird 246 |
. . . 4
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈
FinIa) |
53 | 52 | ex 449 |
. . 3
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
54 | 53 | exlimiv 1845 |
. 2
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
55 | 3, 54 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |