Step | Hyp | Ref
| Expression |
1 | | ensym 8605 |
. . 3
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
2 | | bren 8565 |
. . 3
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
3 | 1, 2 | sylib 221 |
. 2
⊢ (𝐴 ≈ 𝐵 → ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
4 | | elpwi 4498 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵) |
5 | | simplr 769 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐴 ∈ FinIa) |
6 | | imassrn 5915 |
. . . . . . . . . 10
⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓 |
7 | | f1of 6619 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵⟶𝐴) |
8 | 7 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵⟶𝐴) |
9 | 8 | frnd 6513 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ran 𝑓 ⊆ 𝐴) |
10 | 6, 9 | sstrid 3889 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ⊆ 𝐴) |
11 | | fin1ai 9794 |
. . . . . . . . 9
⊢ ((𝐴 ∈ FinIa ∧
(𝑓 “ 𝑥) ⊆ 𝐴) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
12 | 5, 10, 11 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
13 | | f1of1 6618 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
14 | 13 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵–1-1→𝐴) |
15 | | simpr 488 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) |
16 | | vex 3402 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ V) |
18 | | f1imaeng 8616 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑥) ≈ 𝑥) |
19 | 14, 15, 17, 18 | syl3anc 1372 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
20 | | enfi 8786 |
. . . . . . . . . 10
⊢ ((𝑓 “ 𝑥) ≈ 𝑥 → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
22 | | df-f1 6345 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ Fun ◡𝑓)) |
23 | 22 | simprbi 500 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1→𝐴 → Fun ◡𝑓) |
24 | | imadif 6424 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝑓 → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
25 | 14, 23, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
26 | | f1ofo 6626 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–onto→𝐴) |
27 | | foima 6598 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
29 | 28 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
30 | 29 | difeq1d 4013 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
31 | 25, 30 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
32 | | difssd 4024 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ⊆ 𝐵) |
33 | | vex 3402 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
34 | 7 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝑓:𝐵⟶𝐴) |
35 | | dmfex 7639 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ V) |
36 | 33, 34, 35 | sylancr 590 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈ V) |
37 | 36 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐵 ∈ V) |
38 | 37 | difexd 5198 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ∈ V) |
39 | | f1imaeng 8616 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝐵 ∖ 𝑥) ⊆ 𝐵 ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
40 | 14, 32, 38, 39 | syl3anc 1372 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
41 | 31, 40 | eqbrtrrd 5055 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
42 | | enfi 8786 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
44 | 21, 43 | orbi12d 918 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin) ↔ (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
45 | 12, 44 | mpbid 235 |
. . . . . . 7
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
46 | 4, 45 | sylan2 596 |
. . . . . 6
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
47 | 46 | ralrimiva 3096 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) →
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
48 | | isfin1a 9793 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
49 | 36, 48 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
50 | 47, 49 | mpbird 260 |
. . . 4
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈
FinIa) |
51 | 50 | ex 416 |
. . 3
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
52 | 51 | exlimiv 1936 |
. 2
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
53 | 3, 52 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |