Proof of Theorem cfsetsnfsetf
Step | Hyp | Ref
| Expression |
1 | | simpl 486 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐴 ∈ 𝑉) |
2 | 1 | adantr 484 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → 𝐴 ∈ 𝑉) |
3 | 2 | mptexd 7049 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∈ V) |
4 | | vex 3419 |
. . . . . . . . . . 11
⊢ 𝑔 ∈ V |
5 | | feq1 6535 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑔 → (𝑥:{𝑌}⟶𝐵 ↔ 𝑔:{𝑌}⟶𝐵)) |
6 | | cfsetsnfsetfv.g |
. . . . . . . . . . 11
⊢ 𝐺 = {𝑥 ∣ 𝑥:{𝑌}⟶𝐵} |
7 | 4, 5, 6 | elab2 3598 |
. . . . . . . . . 10
⊢ (𝑔 ∈ 𝐺 ↔ 𝑔:{𝑌}⟶𝐵) |
8 | 7 | biimpi 219 |
. . . . . . . . 9
⊢ (𝑔 ∈ 𝐺 → 𝑔:{𝑌}⟶𝐵) |
9 | 8 | adantl 485 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → 𝑔:{𝑌}⟶𝐵) |
10 | | snidg 4584 |
. . . . . . . . . 10
⊢ (𝑌 ∈ 𝐴 → 𝑌 ∈ {𝑌}) |
11 | 10 | adantl 485 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝑌 ∈ {𝑌}) |
12 | 11 | adantr 484 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → 𝑌 ∈ {𝑌}) |
13 | 9, 12 | ffvelrnd 6914 |
. . . . . . 7
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → (𝑔‘𝑌) ∈ 𝐵) |
14 | 13 | adantr 484 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) ∧ 𝑎 ∈ 𝐴) → (𝑔‘𝑌) ∈ 𝐵) |
15 | 14 | fmpttd 6941 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)):𝐴⟶𝐵) |
16 | | eqeq2 2750 |
. . . . . . . 8
⊢ (𝑏 = (𝑔‘𝑌) → ((𝑔‘𝑌) = 𝑏 ↔ (𝑔‘𝑌) = (𝑔‘𝑌))) |
17 | 16 | ralbidv 3119 |
. . . . . . 7
⊢ (𝑏 = (𝑔‘𝑌) → (∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏 ↔ ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = (𝑔‘𝑌))) |
18 | 17 | adantl 485 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) ∧ 𝑏 = (𝑔‘𝑌)) → (∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏 ↔ ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = (𝑔‘𝑌))) |
19 | | eqidd 2739 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑌) = (𝑔‘𝑌)) |
20 | 19 | ralrimiva 3106 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = (𝑔‘𝑌)) |
21 | 13, 18, 20 | rspcedvd 3547 |
. . . . 5
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏) |
22 | 15, 21 | jca 515 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → ((𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)):𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏)) |
23 | | feq1 6535 |
. . . . 5
⊢ (𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) → (𝑓:𝐴⟶𝐵 ↔ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)):𝐴⟶𝐵)) |
24 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) → 𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) |
25 | | eqidd 2739 |
. . . . . . . . 9
⊢ (((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) ∧ 𝑎 = 𝑧) → (𝑔‘𝑌) = (𝑔‘𝑌)) |
26 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ 𝐴) |
27 | | fvexd 6741 |
. . . . . . . . 9
⊢ ((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) → (𝑔‘𝑌) ∈ V) |
28 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎𝑓 |
29 | | nfmpt1 5162 |
. . . . . . . . . . 11
⊢
Ⅎ𝑎(𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) |
30 | 28, 29 | nfeq 2918 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) |
31 | | nfv 1922 |
. . . . . . . . . 10
⊢
Ⅎ𝑎 𝑧 ∈ 𝐴 |
32 | 30, 31 | nfan 1907 |
. . . . . . . . 9
⊢
Ⅎ𝑎(𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) |
33 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑎𝑧 |
34 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑎(𝑔‘𝑌) |
35 | 24, 25, 26, 27, 32, 33, 34 | fvmptdf 6833 |
. . . . . . . 8
⊢ ((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) → (𝑓‘𝑧) = (𝑔‘𝑌)) |
36 | 35 | eqeq1d 2740 |
. . . . . . 7
⊢ ((𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∧ 𝑧 ∈ 𝐴) → ((𝑓‘𝑧) = 𝑏 ↔ (𝑔‘𝑌) = 𝑏)) |
37 | 36 | ralbidva 3118 |
. . . . . 6
⊢ (𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) → (∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏 ↔ ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏)) |
38 | 37 | rexbidv 3223 |
. . . . 5
⊢ (𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) → (∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏 ↔ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏)) |
39 | 23, 38 | anbi12d 634 |
. . . 4
⊢ (𝑓 = (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) → ((𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏) ↔ ((𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)):𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑔‘𝑌) = 𝑏))) |
40 | 3, 22, 39 | elabd 3597 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∈ {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)}) |
41 | | cfsetsnfsetfv.f |
. . 3
⊢ 𝐹 = {𝑓 ∣ (𝑓:𝐴⟶𝐵 ∧ ∃𝑏 ∈ 𝐵 ∀𝑧 ∈ 𝐴 (𝑓‘𝑧) = 𝑏)} |
42 | 40, 41 | eleqtrrdi 2850 |
. 2
⊢ (((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) ∧ 𝑔 ∈ 𝐺) → (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌)) ∈ 𝐹) |
43 | | cfsetsnfsetfv.h |
. 2
⊢ 𝐻 = (𝑔 ∈ 𝐺 ↦ (𝑎 ∈ 𝐴 ↦ (𝑔‘𝑌))) |
44 | 42, 43 | fmptd 6940 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ 𝑌 ∈ 𝐴) → 𝐻:𝐺⟶𝐹) |