Step | Hyp | Ref
| Expression |
1 | | ensym 8789 |
. . 3
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
2 | | bren 8743 |
. . 3
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
3 | 1, 2 | sylib 217 |
. 2
⊢ (𝐴 ≈ 𝐵 → ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
4 | | elpwi 4542 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵) |
5 | | simplr 766 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐴 ∈ FinIa) |
6 | | imassrn 5980 |
. . . . . . . . . 10
⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓 |
7 | | f1of 6716 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵⟶𝐴) |
8 | 7 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵⟶𝐴) |
9 | 8 | frnd 6608 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ran 𝑓 ⊆ 𝐴) |
10 | 6, 9 | sstrid 3932 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ⊆ 𝐴) |
11 | | fin1ai 10049 |
. . . . . . . . 9
⊢ ((𝐴 ∈ FinIa ∧
(𝑓 “ 𝑥) ⊆ 𝐴) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
12 | 5, 10, 11 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
13 | | f1of1 6715 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
14 | 13 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵–1-1→𝐴) |
15 | | simpr 485 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) |
16 | | vex 3436 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ V) |
18 | | f1imaeng 8800 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑥) ≈ 𝑥) |
19 | 14, 15, 17, 18 | syl3anc 1370 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
20 | | enfi 8973 |
. . . . . . . . . 10
⊢ ((𝑓 “ 𝑥) ≈ 𝑥 → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
22 | | df-f1 6438 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ Fun ◡𝑓)) |
23 | 22 | simprbi 497 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1→𝐴 → Fun ◡𝑓) |
24 | | imadif 6518 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝑓 → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
25 | 14, 23, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
26 | | f1ofo 6723 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–onto→𝐴) |
27 | | foima 6693 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
29 | 28 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
30 | 29 | difeq1d 4056 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
31 | 25, 30 | eqtrd 2778 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
32 | | difssd 4067 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ⊆ 𝐵) |
33 | | vex 3436 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
34 | 7 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝑓:𝐵⟶𝐴) |
35 | | dmfex 7754 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ V) |
36 | 33, 34, 35 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈ V) |
37 | 36 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐵 ∈ V) |
38 | 37 | difexd 5253 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ∈ V) |
39 | | f1imaeng 8800 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝐵 ∖ 𝑥) ⊆ 𝐵 ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
40 | 14, 32, 38, 39 | syl3anc 1370 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
41 | 31, 40 | eqbrtrrd 5098 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
42 | | enfi 8973 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
43 | 41, 42 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
44 | 21, 43 | orbi12d 916 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin) ↔ (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
45 | 12, 44 | mpbid 231 |
. . . . . . 7
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
46 | 4, 45 | sylan2 593 |
. . . . . 6
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
47 | 46 | ralrimiva 3103 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) →
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
48 | | isfin1a 10048 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
49 | 36, 48 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
50 | 47, 49 | mpbird 256 |
. . . 4
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈
FinIa) |
51 | 50 | ex 413 |
. . 3
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
52 | 51 | exlimiv 1933 |
. 2
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
53 | 3, 52 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |