Proof of Theorem f1oresf1o2
Step | Hyp | Ref
| Expression |
1 | | f1oresf1o2.1 |
. 2
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→𝐵) |
2 | | f1oresf1o2.2 |
. 2
⊢ (𝜑 → 𝐷 ⊆ 𝐴) |
3 | | f1of 6619 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴⟶𝐵) |
4 | 1, 3 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
5 | 4 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝐹:𝐴⟶𝐵) |
6 | 2 | sselda 3878 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → 𝑥 ∈ 𝐴) |
7 | 5, 6 | jca 515 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷) → (𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴)) |
8 | 7 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → (𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴)) |
9 | | ffvelrn 6860 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
10 | 8, 9 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → (𝐹‘𝑥) ∈ 𝐵) |
11 | | eleq1 2820 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑦 → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
12 | 11 | 3ad2ant3 1136 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → ((𝐹‘𝑥) ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
13 | 10, 12 | mpbid 235 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → 𝑦 ∈ 𝐵) |
14 | | eqcom 2745 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
15 | | f1oresf1o2.3 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 ↔ 𝜒)) |
16 | 15 | biimpd 232 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 → 𝜒)) |
17 | 16 | ex 416 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 = (𝐹‘𝑥) → (𝑥 ∈ 𝐷 → 𝜒))) |
18 | 14, 17 | syl5bi 245 |
. . . . . . 7
⊢ (𝜑 → ((𝐹‘𝑥) = 𝑦 → (𝑥 ∈ 𝐷 → 𝜒))) |
19 | 18 | com23 86 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐷 → ((𝐹‘𝑥) = 𝑦 → 𝜒))) |
20 | 19 | 3imp 1112 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → 𝜒) |
21 | 13, 20 | jca 515 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → (𝑦 ∈ 𝐵 ∧ 𝜒)) |
22 | 21 | rexlimdv3a 3196 |
. . 3
⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 → (𝑦 ∈ 𝐵 ∧ 𝜒))) |
23 | | f1ofo 6626 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐵 → 𝐹:𝐴–onto→𝐵) |
24 | 1, 23 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴–onto→𝐵) |
25 | | foelrni 6732 |
. . . . . . 7
⊢ ((𝐹:𝐴–onto→𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
26 | 24, 25 | sylan 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦) |
27 | 26 | ex 416 |
. . . . 5
⊢ (𝜑 → (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦)) |
28 | | nfv 1920 |
. . . . . 6
⊢
Ⅎ𝑥𝜑 |
29 | | nfv 1920 |
. . . . . . 7
⊢
Ⅎ𝑥𝜒 |
30 | | nfre1 3216 |
. . . . . . 7
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 |
31 | 29, 30 | nfim 1902 |
. . . . . 6
⊢
Ⅎ𝑥(𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦) |
32 | | rspe 3214 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ 𝐷 ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦) |
33 | 32 | expcom 417 |
. . . . . . . . . . . . 13
⊢ ((𝐹‘𝑥) = 𝑦 → (𝑥 ∈ 𝐷 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)) |
34 | 33 | eqcoms 2746 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑥) → (𝑥 ∈ 𝐷 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)) |
35 | 34 | adantl 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝑥 ∈ 𝐷 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)) |
36 | 15, 35 | sylbird 263 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 = (𝐹‘𝑥)) → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)) |
37 | 36 | ex 416 |
. . . . . . . . 9
⊢ (𝜑 → (𝑦 = (𝐹‘𝑥) → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦))) |
38 | 37 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦))) |
39 | 14, 38 | syl5bi 245 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦))) |
40 | 39 | ex 416 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 → ((𝐹‘𝑥) = 𝑦 → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)))) |
41 | 28, 31, 40 | rexlimd 3227 |
. . . . 5
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝑦 → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦))) |
42 | 27, 41 | syld 47 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐵 → (𝜒 → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦))) |
43 | 42 | impd 414 |
. . 3
⊢ (𝜑 → ((𝑦 ∈ 𝐵 ∧ 𝜒) → ∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦)) |
44 | 22, 43 | impbid 215 |
. 2
⊢ (𝜑 → (∃𝑥 ∈ 𝐷 (𝐹‘𝑥) = 𝑦 ↔ (𝑦 ∈ 𝐵 ∧ 𝜒))) |
45 | 1, 2, 44 | f1oresf1o 44307 |
1
⊢ (𝜑 → (𝐹 ↾ 𝐷):𝐷–1-1-onto→{𝑦 ∈ 𝐵 ∣ 𝜒}) |