| Step | Hyp | Ref
| Expression |
| 1 | | ensym 9043 |
. 2
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
| 2 | | bren 8995 |
. . . 4
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
| 3 | | simpr 484 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → 𝑥 ⊊ 𝐵) |
| 4 | | f1of1 6847 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
| 5 | | pssss 4098 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵) |
| 6 | | ssid 4006 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ 𝐵 |
| 7 | 5, 6 | jctir 520 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊊ 𝐵 → (𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) |
| 8 | | f1imapss 7286 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ 𝑥 ⊊ 𝐵)) |
| 9 | 4, 7, 8 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ 𝑥 ⊊ 𝐵)) |
| 10 | 3, 9 | mpbird 257 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵)) |
| 11 | | imadmrn 6088 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
| 12 | | f1odm 6852 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → dom 𝑓 = 𝐵) |
| 13 | 12 | imaeq2d 6078 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ 𝐵)) |
| 14 | | dff1o5 6857 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 ↔ (𝑓:𝐵–1-1→𝐴 ∧ ran 𝑓 = 𝐴)) |
| 15 | 14 | simprbi 496 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → ran 𝑓 = 𝐴) |
| 16 | 11, 13, 15 | 3eqtr3a 2801 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
| 17 | 16 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
| 18 | 17 | psseq2d 4096 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ (𝑓 “ 𝑥) ⊊ 𝐴)) |
| 19 | 10, 18 | mpbid 232 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ⊊ 𝐴) |
| 20 | 19 | adantrr 717 |
. . . . . . . . 9
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ⊊ 𝐴) |
| 21 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 22 | 21 | f1imaen 9057 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 23 | 4, 5, 22 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 24 | 23 | adantrr 717 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝑥) |
| 25 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝑥 ≈ 𝐵) |
| 26 | | entr 9046 |
. . . . . . . . . . 11
⊢ (((𝑓 “ 𝑥) ≈ 𝑥 ∧ 𝑥 ≈ 𝐵) → (𝑓 “ 𝑥) ≈ 𝐵) |
| 27 | 24, 25, 26 | syl2anc 584 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝐵) |
| 28 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
| 29 | | f1oen3g 9007 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵–1-1-onto→𝐴) → 𝐵 ≈ 𝐴) |
| 30 | 28, 29 | mpan 690 |
. . . . . . . . . . 11
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝐵 ≈ 𝐴) |
| 31 | 30 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝐵 ≈ 𝐴) |
| 32 | | entr 9046 |
. . . . . . . . . 10
⊢ (((𝑓 “ 𝑥) ≈ 𝐵 ∧ 𝐵 ≈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝐴) |
| 33 | 27, 31, 32 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝐴) |
| 34 | | fin4i 10338 |
. . . . . . . . 9
⊢ (((𝑓 “ 𝑥) ⊊ 𝐴 ∧ (𝑓 “ 𝑥) ≈ 𝐴) → ¬ 𝐴 ∈ FinIV) |
| 35 | 20, 33, 34 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → ¬ 𝐴 ∈ FinIV) |
| 36 | 35 | ex 412 |
. . . . . . 7
⊢ (𝑓:𝐵–1-1-onto→𝐴 → ((𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵) → ¬ 𝐴 ∈ FinIV)) |
| 37 | 36 | exlimdv 1933 |
. . . . . 6
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵) → ¬ 𝐴 ∈ FinIV)) |
| 38 | 37 | con2d 134 |
. . . . 5
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 39 | 38 | exlimiv 1930 |
. . . 4
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 40 | 2, 39 | sylbi 217 |
. . 3
⊢ (𝐵 ≈ 𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 41 | | relen 8990 |
. . . . 5
⊢ Rel
≈ |
| 42 | 41 | brrelex1i 5741 |
. . . 4
⊢ (𝐵 ≈ 𝐴 → 𝐵 ∈ V) |
| 43 | | isfin4 10337 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIV ↔
¬ ∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 44 | 42, 43 | syl 17 |
. . 3
⊢ (𝐵 ≈ 𝐴 → (𝐵 ∈ FinIV ↔ ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
| 45 | 40, 44 | sylibrd 259 |
. 2
⊢ (𝐵 ≈ 𝐴 → (𝐴 ∈ FinIV → 𝐵 ∈
FinIV)) |
| 46 | 1, 45 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIV → 𝐵 ∈
FinIV)) |