Step | Hyp | Ref
| Expression |
1 | | ensym 8558 |
. . 3
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
2 | | bren 8518 |
. . 3
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
3 | 1, 2 | sylib 220 |
. 2
⊢ (𝐴 ≈ 𝐵 → ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
4 | | elpwi 4548 |
. . . . . . 7
⊢ (𝑥 ∈ 𝒫 𝐵 → 𝑥 ⊆ 𝐵) |
5 | | simplr 767 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐴 ∈ FinIa) |
6 | | imassrn 5940 |
. . . . . . . . . 10
⊢ (𝑓 “ 𝑥) ⊆ ran 𝑓 |
7 | | f1of 6615 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵⟶𝐴) |
8 | 7 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵⟶𝐴) |
9 | 8 | frnd 6521 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ran 𝑓 ⊆ 𝐴) |
10 | 6, 9 | sstrid 3978 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ⊆ 𝐴) |
11 | | fin1ai 9715 |
. . . . . . . . 9
⊢ ((𝐴 ∈ FinIa ∧
(𝑓 “ 𝑥) ⊆ 𝐴) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
12 | 5, 10, 11 | syl2anc 586 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin)) |
13 | | f1of1 6614 |
. . . . . . . . . . . 12
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
14 | 13 | ad2antrr 724 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑓:𝐵–1-1→𝐴) |
15 | | simpr 487 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ⊆ 𝐵) |
16 | | vex 3497 |
. . . . . . . . . . . 12
⊢ 𝑥 ∈ V |
17 | 16 | a1i 11 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝑥 ∈ V) |
18 | | f1imaeng 8569 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵 ∧ 𝑥 ∈ V) → (𝑓 “ 𝑥) ≈ 𝑥) |
19 | 14, 15, 17, 18 | syl3anc 1367 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
20 | | enfi 8734 |
. . . . . . . . . 10
⊢ ((𝑓 “ 𝑥) ≈ 𝑥 → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
21 | 19, 20 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝑥) ∈ Fin ↔ 𝑥 ∈ Fin)) |
22 | | df-f1 6360 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1→𝐴 ↔ (𝑓:𝐵⟶𝐴 ∧ Fun ◡𝑓)) |
23 | 22 | simprbi 499 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1→𝐴 → Fun ◡𝑓) |
24 | | imadif 6438 |
. . . . . . . . . . . . 13
⊢ (Fun
◡𝑓 → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
25 | 14, 23, 24 | 3syl 18 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥))) |
26 | | f1ofo 6622 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–onto→𝐴) |
27 | | foima 6595 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
29 | 28 | ad2antrr 724 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
30 | 29 | difeq1d 4098 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝑓 “ 𝐵) ∖ (𝑓 “ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
31 | 25, 30 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) = (𝐴 ∖ (𝑓 “ 𝑥))) |
32 | | difssd 4109 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ⊆ 𝐵) |
33 | | vex 3497 |
. . . . . . . . . . . . . . 15
⊢ 𝑓 ∈ V |
34 | 7 | adantr 483 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝑓:𝐵⟶𝐴) |
35 | | dmfex 7641 |
. . . . . . . . . . . . . . 15
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵⟶𝐴) → 𝐵 ∈ V) |
36 | 33, 34, 35 | sylancr 589 |
. . . . . . . . . . . . . 14
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈ V) |
37 | 36 | adantr 483 |
. . . . . . . . . . . . 13
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → 𝐵 ∈ V) |
38 | | difexg 5231 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ V → (𝐵 ∖ 𝑥) ∈ V) |
39 | 37, 38 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐵 ∖ 𝑥) ∈ V) |
40 | | f1imaeng 8569 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝐵 ∖ 𝑥) ⊆ 𝐵 ∧ (𝐵 ∖ 𝑥) ∈ V) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
41 | 14, 32, 39, 40 | syl3anc 1367 |
. . . . . . . . . . 11
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ (𝐵 ∖ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
42 | 31, 41 | eqbrtrrd 5090 |
. . . . . . . . . 10
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥)) |
43 | | enfi 8734 |
. . . . . . . . . 10
⊢ ((𝐴 ∖ (𝑓 “ 𝑥)) ≈ (𝐵 ∖ 𝑥) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
44 | 42, 43 | syl 17 |
. . . . . . . . 9
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → ((𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin ↔ (𝐵 ∖ 𝑥) ∈ Fin)) |
45 | 21, 44 | orbi12d 915 |
. . . . . . . 8
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (((𝑓 “ 𝑥) ∈ Fin ∨ (𝐴 ∖ (𝑓 “ 𝑥)) ∈ Fin) ↔ (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
46 | 12, 45 | mpbid 234 |
. . . . . . 7
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ⊆ 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
47 | 4, 46 | sylan2 594 |
. . . . . 6
⊢ (((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) ∧ 𝑥 ∈ 𝒫 𝐵) → (𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
48 | 47 | ralrimiva 3182 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) →
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin)) |
49 | | isfin1a 9714 |
. . . . . 6
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
50 | 36, 49 | syl 17 |
. . . . 5
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → (𝐵 ∈ FinIa ↔
∀𝑥 ∈ 𝒫
𝐵(𝑥 ∈ Fin ∨ (𝐵 ∖ 𝑥) ∈ Fin))) |
51 | 48, 50 | mpbird 259 |
. . . 4
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝐴 ∈ FinIa) → 𝐵 ∈
FinIa) |
52 | 51 | ex 415 |
. . 3
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
53 | 52 | exlimiv 1931 |
. 2
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |
54 | 3, 53 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIa → 𝐵 ∈
FinIa)) |