Proof of Theorem f1oresrab
| Step | Hyp | Ref
| Expression |
| 1 | | f1oresrab.2 |
. . . 4
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
| 2 | | f1ofun 6850 |
. . . 4
⊢ (𝐹:𝐴–1-1-onto→𝐵 → Fun 𝐹) |
| 3 | | funcnvcnv 6633 |
. . . 4
⊢ (Fun
𝐹 → Fun ◡◡𝐹) |
| 4 | 1, 2, 3 | 3syl 18 |
. . 3
⊢ (𝜑 → Fun ◡◡𝐹) |
| 5 | | f1ocnv 6860 |
. . . . . 6
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) |
| 6 | | f1of1 6847 |
. . . . . 6
⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵–1-1→𝐴) |
| 7 | 1, 5, 6 | 3syl 18 |
. . . . 5
⊢ (𝜑 → ◡𝐹:𝐵–1-1→𝐴) |
| 8 | | ssrab2 4080 |
. . . . 5
⊢ {𝑦 ∈ 𝐵 ∣ 𝜒} ⊆ 𝐵 |
| 9 | | f1ores 6862 |
. . . . 5
⊢ ((◡𝐹:𝐵–1-1→𝐴 ∧ {𝑦 ∈ 𝐵 ∣ 𝜒} ⊆ 𝐵) → (◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→(◡𝐹 “ {𝑦 ∈ 𝐵 ∣ 𝜒})) |
| 10 | 7, 8, 9 | sylancl 586 |
. . . 4
⊢ (𝜑 → (◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→(◡𝐹 “ {𝑦 ∈ 𝐵 ∣ 𝜒})) |
| 11 | | f1oresrab.1 |
. . . . . . 7
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐶) |
| 12 | 11 | mptpreima 6258 |
. . . . . 6
⊢ (◡𝐹 “ {𝑦 ∈ 𝐵 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ {𝑦 ∈ 𝐵 ∣ 𝜒}} |
| 13 | | f1oresrab.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐶) → (𝜒 ↔ 𝜓)) |
| 14 | 13 | 3expia 1122 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐶 → (𝜒 ↔ 𝜓))) |
| 15 | 14 | alrimiv 1927 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑦(𝑦 = 𝐶 → (𝜒 ↔ 𝜓))) |
| 16 | | f1of 6848 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
| 17 | 1, 16 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
| 18 | 11 | fmpt 7130 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝐴 𝐶 ∈ 𝐵 ↔ 𝐹:𝐴⟶𝐵) |
| 19 | 17, 18 | sylibr 234 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐶 ∈ 𝐵) |
| 20 | 19 | r19.21bi 3251 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝐵) |
| 21 | | elrab3t 3691 |
. . . . . . . 8
⊢
((∀𝑦(𝑦 = 𝐶 → (𝜒 ↔ 𝜓)) ∧ 𝐶 ∈ 𝐵) → (𝐶 ∈ {𝑦 ∈ 𝐵 ∣ 𝜒} ↔ 𝜓)) |
| 22 | 15, 20, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐶 ∈ {𝑦 ∈ 𝐵 ∣ 𝜒} ↔ 𝜓)) |
| 23 | 22 | rabbidva 3443 |
. . . . . 6
⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝐶 ∈ {𝑦 ∈ 𝐵 ∣ 𝜒}} = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
| 24 | 12, 23 | eqtrid 2789 |
. . . . 5
⊢ (𝜑 → (◡𝐹 “ {𝑦 ∈ 𝐵 ∣ 𝜒}) = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
| 25 | 24 | f1oeq3d 6845 |
. . . 4
⊢ (𝜑 → ((◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→(◡𝐹 “ {𝑦 ∈ 𝐵 ∣ 𝜒}) ↔ (◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→{𝑥 ∈ 𝐴 ∣ 𝜓})) |
| 26 | 10, 25 | mpbid 232 |
. . 3
⊢ (𝜑 → (◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→{𝑥 ∈ 𝐴 ∣ 𝜓}) |
| 27 | | f1orescnv 6863 |
. . 3
⊢ ((Fun
◡◡𝐹 ∧ (◡𝐹 ↾ {𝑦 ∈ 𝐵 ∣ 𝜒}):{𝑦 ∈ 𝐵 ∣ 𝜒}–1-1-onto→{𝑥 ∈ 𝐴 ∣ 𝜓}) → (◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |
| 28 | 4, 26, 27 | syl2anc 584 |
. 2
⊢ (𝜑 → (◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |
| 29 | | rescnvcnv 6224 |
. . 3
⊢ (◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}) = (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}) |
| 30 | | f1oeq1 6836 |
. . 3
⊢ ((◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}) = (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}) → ((◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒} ↔ (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒})) |
| 31 | 29, 30 | ax-mp 5 |
. 2
⊢ ((◡◡𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒} ↔ (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |
| 32 | 28, 31 | sylib 218 |
1
⊢ (𝜑 → (𝐹 ↾ {𝑥 ∈ 𝐴 ∣ 𝜓}):{𝑥 ∈ 𝐴 ∣ 𝜓}–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |