Step | Hyp | Ref
| Expression |
1 | | ensym 8351 |
. 2
⊢ (𝐴 ≈ 𝐵 → 𝐵 ≈ 𝐴) |
2 | | bren 8311 |
. . . 4
⊢ (𝐵 ≈ 𝐴 ↔ ∃𝑓 𝑓:𝐵–1-1-onto→𝐴) |
3 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → 𝑥 ⊊ 𝐵) |
4 | | f1of1 6441 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝑓:𝐵–1-1→𝐴) |
5 | | pssss 3961 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ⊊ 𝐵 → 𝑥 ⊆ 𝐵) |
6 | | ssid 3878 |
. . . . . . . . . . . . . 14
⊢ 𝐵 ⊆ 𝐵 |
7 | 5, 6 | jctir 513 |
. . . . . . . . . . . . 13
⊢ (𝑥 ⊊ 𝐵 → (𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) |
8 | | f1imapss 6847 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ (𝑥 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐵)) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ 𝑥 ⊊ 𝐵)) |
9 | 4, 7, 8 | syl2an 586 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ 𝑥 ⊊ 𝐵)) |
10 | 3, 9 | mpbird 249 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵)) |
11 | | imadmrn 5778 |
. . . . . . . . . . . . . 14
⊢ (𝑓 “ dom 𝑓) = ran 𝑓 |
12 | | f1odm 6446 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 → dom 𝑓 = 𝐵) |
13 | 12 | imaeq2d 5768 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ dom 𝑓) = (𝑓 “ 𝐵)) |
14 | | dff1o5 6451 |
. . . . . . . . . . . . . . 15
⊢ (𝑓:𝐵–1-1-onto→𝐴 ↔ (𝑓:𝐵–1-1→𝐴 ∧ ran 𝑓 = 𝐴)) |
15 | 14 | simprbi 489 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝐵–1-1-onto→𝐴 → ran 𝑓 = 𝐴) |
16 | 11, 13, 15 | 3eqtr3a 2835 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝑓 “ 𝐵) = 𝐴) |
17 | 16 | adantr 473 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝐵) = 𝐴) |
18 | 17 | psseq2d 3959 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → ((𝑓 “ 𝑥) ⊊ (𝑓 “ 𝐵) ↔ (𝑓 “ 𝑥) ⊊ 𝐴)) |
19 | 10, 18 | mpbid 224 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ⊊ 𝐴) |
20 | 19 | adantrr 704 |
. . . . . . . . 9
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ⊊ 𝐴) |
21 | | vex 3415 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
22 | 21 | f1imaen 8364 |
. . . . . . . . . . . . 13
⊢ ((𝑓:𝐵–1-1→𝐴 ∧ 𝑥 ⊆ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
23 | 4, 5, 22 | syl2an 586 |
. . . . . . . . . . . 12
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ 𝑥 ⊊ 𝐵) → (𝑓 “ 𝑥) ≈ 𝑥) |
24 | 23 | adantrr 704 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝑥) |
25 | | simprr 760 |
. . . . . . . . . . 11
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝑥 ≈ 𝐵) |
26 | | entr 8354 |
. . . . . . . . . . 11
⊢ (((𝑓 “ 𝑥) ≈ 𝑥 ∧ 𝑥 ≈ 𝐵) → (𝑓 “ 𝑥) ≈ 𝐵) |
27 | 24, 25, 26 | syl2anc 576 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝐵) |
28 | | vex 3415 |
. . . . . . . . . . . 12
⊢ 𝑓 ∈ V |
29 | | f1oen3g 8318 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ V ∧ 𝑓:𝐵–1-1-onto→𝐴) → 𝐵 ≈ 𝐴) |
30 | 28, 29 | mpan 677 |
. . . . . . . . . . 11
⊢ (𝑓:𝐵–1-1-onto→𝐴 → 𝐵 ≈ 𝐴) |
31 | 30 | adantr 473 |
. . . . . . . . . 10
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → 𝐵 ≈ 𝐴) |
32 | | entr 8354 |
. . . . . . . . . 10
⊢ (((𝑓 “ 𝑥) ≈ 𝐵 ∧ 𝐵 ≈ 𝐴) → (𝑓 “ 𝑥) ≈ 𝐴) |
33 | 27, 31, 32 | syl2anc 576 |
. . . . . . . . 9
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → (𝑓 “ 𝑥) ≈ 𝐴) |
34 | | fin4i 9514 |
. . . . . . . . 9
⊢ (((𝑓 “ 𝑥) ⊊ 𝐴 ∧ (𝑓 “ 𝑥) ≈ 𝐴) → ¬ 𝐴 ∈ FinIV) |
35 | 20, 33, 34 | syl2anc 576 |
. . . . . . . 8
⊢ ((𝑓:𝐵–1-1-onto→𝐴 ∧ (𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵)) → ¬ 𝐴 ∈ FinIV) |
36 | 35 | ex 405 |
. . . . . . 7
⊢ (𝑓:𝐵–1-1-onto→𝐴 → ((𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵) → ¬ 𝐴 ∈ FinIV)) |
37 | 36 | exlimdv 1892 |
. . . . . 6
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵) → ¬ 𝐴 ∈ FinIV)) |
38 | 37 | con2d 132 |
. . . . 5
⊢ (𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
39 | 38 | exlimiv 1889 |
. . . 4
⊢
(∃𝑓 𝑓:𝐵–1-1-onto→𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
40 | 2, 39 | sylbi 209 |
. . 3
⊢ (𝐵 ≈ 𝐴 → (𝐴 ∈ FinIV → ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
41 | | relen 8307 |
. . . . 5
⊢ Rel
≈ |
42 | 41 | brrelex1i 5455 |
. . . 4
⊢ (𝐵 ≈ 𝐴 → 𝐵 ∈ V) |
43 | | isfin4 9513 |
. . . 4
⊢ (𝐵 ∈ V → (𝐵 ∈ FinIV ↔
¬ ∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
44 | 42, 43 | syl 17 |
. . 3
⊢ (𝐵 ≈ 𝐴 → (𝐵 ∈ FinIV ↔ ¬
∃𝑥(𝑥 ⊊ 𝐵 ∧ 𝑥 ≈ 𝐵))) |
45 | 40, 44 | sylibrd 251 |
. 2
⊢ (𝐵 ≈ 𝐴 → (𝐴 ∈ FinIV → 𝐵 ∈
FinIV)) |
46 | 1, 45 | syl 17 |
1
⊢ (𝐴 ≈ 𝐵 → (𝐴 ∈ FinIV → 𝐵 ∈
FinIV)) |