ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  cc2lem GIF version

Theorem cc2lem 7240
Description: Lemma for cc2 7241. (Contributed by Jim Kingdon, 27-Apr-2024.)
Hypotheses
Ref Expression
cc2.cc (πœ‘ β†’ CCHOICE)
cc2.a (πœ‘ β†’ 𝐹 Fn Ο‰)
cc2.m (πœ‘ β†’ βˆ€π‘₯ ∈ Ο‰ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘₯))
cc2lem.a 𝐴 = (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΉβ€˜π‘›)))
cc2lem.g 𝐺 = (𝑛 ∈ Ο‰ ↦ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
Assertion
Ref Expression
cc2lem (πœ‘ β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)))
Distinct variable groups:   𝐴,𝑓,𝑛   𝑀,𝐴,𝑛   𝑛,𝐹,𝑀   𝑓,𝐹,𝑔,𝑛   π‘₯,𝐹,𝑛,𝑀   𝑔,𝐺,𝑛   πœ‘,𝑛,𝑀   πœ‘,𝑓
Allowed substitution hints:   πœ‘(π‘₯,𝑔)   𝐴(π‘₯,𝑔)   𝐺(π‘₯,𝑀,𝑓)

Proof of Theorem cc2lem
Dummy variables 𝑧 π‘˜ π‘Ž are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cc2.cc . . 3 (πœ‘ β†’ CCHOICE)
2 vex 2738 . . . . . . . 8 𝑛 ∈ V
32snex 4180 . . . . . . 7 {𝑛} ∈ V
4 cc2.a . . . . . . . 8 (πœ‘ β†’ 𝐹 Fn Ο‰)
5 funfvex 5524 . . . . . . . . 9 ((Fun 𝐹 ∧ 𝑛 ∈ dom 𝐹) β†’ (πΉβ€˜π‘›) ∈ V)
65funfni 5308 . . . . . . . 8 ((𝐹 Fn Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ (πΉβ€˜π‘›) ∈ V)
74, 6sylan 283 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (πΉβ€˜π‘›) ∈ V)
8 xpexg 4734 . . . . . . 7 (({𝑛} ∈ V ∧ (πΉβ€˜π‘›) ∈ V) β†’ ({𝑛} Γ— (πΉβ€˜π‘›)) ∈ V)
93, 7, 8sylancr 414 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ ({𝑛} Γ— (πΉβ€˜π‘›)) ∈ V)
10 cc2lem.a . . . . . 6 𝐴 = (𝑛 ∈ Ο‰ ↦ ({𝑛} Γ— (πΉβ€˜π‘›)))
119, 10fmptd 5662 . . . . 5 (πœ‘ β†’ 𝐴:Ο‰βŸΆV)
12 sneq 3600 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ {𝑛} = {π‘˜})
13 fveq2 5507 . . . . . . . . . 10 (𝑛 = π‘˜ β†’ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))
1412, 13xpeq12d 4645 . . . . . . . . 9 (𝑛 = π‘˜ β†’ ({𝑛} Γ— (πΉβ€˜π‘›)) = ({π‘˜} Γ— (πΉβ€˜π‘˜)))
15 simprr 531 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ π‘˜ ∈ Ο‰)
16 vex 2738 . . . . . . . . . . 11 π‘˜ ∈ V
1716snex 4180 . . . . . . . . . 10 {π‘˜} ∈ V
184adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ 𝐹 Fn Ο‰)
19 funfvex 5524 . . . . . . . . . . . 12 ((Fun 𝐹 ∧ π‘˜ ∈ dom 𝐹) β†’ (πΉβ€˜π‘˜) ∈ V)
2019funfni 5308 . . . . . . . . . . 11 ((𝐹 Fn Ο‰ ∧ π‘˜ ∈ Ο‰) β†’ (πΉβ€˜π‘˜) ∈ V)
2118, 15, 20syl2anc 411 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ (πΉβ€˜π‘˜) ∈ V)
22 xpexg 4734 . . . . . . . . . 10 (({π‘˜} ∈ V ∧ (πΉβ€˜π‘˜) ∈ V) β†’ ({π‘˜} Γ— (πΉβ€˜π‘˜)) ∈ V)
2317, 21, 22sylancr 414 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ ({π‘˜} Γ— (πΉβ€˜π‘˜)) ∈ V)
2410, 14, 15, 23fvmptd3 5601 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ (π΄β€˜π‘˜) = ({π‘˜} Γ— (πΉβ€˜π‘˜)))
2524eqeq2d 2187 . . . . . . 7 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) ↔ (π΄β€˜π‘›) = ({π‘˜} Γ— (πΉβ€˜π‘˜))))
26 simpr 110 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ 𝑛 ∈ Ο‰)
2710fvmpt2 5591 . . . . . . . . . . 11 ((𝑛 ∈ Ο‰ ∧ ({𝑛} Γ— (πΉβ€˜π‘›)) ∈ V) β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΉβ€˜π‘›)))
2826, 9, 27syl2anc 411 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΉβ€˜π‘›)))
2928adantrr 479 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ (π΄β€˜π‘›) = ({𝑛} Γ— (πΉβ€˜π‘›)))
3029eqeq1d 2184 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ ((π΄β€˜π‘›) = ({π‘˜} Γ— (πΉβ€˜π‘˜)) ↔ ({𝑛} Γ— (πΉβ€˜π‘›)) = ({π‘˜} Γ— (πΉβ€˜π‘˜))))
312snm 3709 . . . . . . . . . 10 βˆƒπ‘€ 𝑀 ∈ {𝑛}
32 fveq2 5507 . . . . . . . . . . . . 13 (π‘₯ = 𝑛 β†’ (πΉβ€˜π‘₯) = (πΉβ€˜π‘›))
3332eleq2d 2245 . . . . . . . . . . . 12 (π‘₯ = 𝑛 β†’ (𝑀 ∈ (πΉβ€˜π‘₯) ↔ 𝑀 ∈ (πΉβ€˜π‘›)))
3433exbidv 1823 . . . . . . . . . . 11 (π‘₯ = 𝑛 β†’ (βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘₯) ↔ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘›)))
35 cc2.m . . . . . . . . . . . 12 (πœ‘ β†’ βˆ€π‘₯ ∈ Ο‰ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘₯))
3635adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ βˆ€π‘₯ ∈ Ο‰ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘₯))
37 simprl 529 . . . . . . . . . . 11 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ 𝑛 ∈ Ο‰)
3834, 36, 37rspcdva 2844 . . . . . . . . . 10 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘›))
39 xp11m 5059 . . . . . . . . . 10 ((βˆƒπ‘€ 𝑀 ∈ {𝑛} ∧ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘›)) β†’ (({𝑛} Γ— (πΉβ€˜π‘›)) = ({π‘˜} Γ— (πΉβ€˜π‘˜)) ↔ ({𝑛} = {π‘˜} ∧ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))))
4031, 38, 39sylancr 414 . . . . . . . . 9 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ (({𝑛} Γ— (πΉβ€˜π‘›)) = ({π‘˜} Γ— (πΉβ€˜π‘˜)) ↔ ({𝑛} = {π‘˜} ∧ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜))))
412sneqr 3756 . . . . . . . . . 10 ({𝑛} = {π‘˜} β†’ 𝑛 = π‘˜)
4241adantr 276 . . . . . . . . 9 (({𝑛} = {π‘˜} ∧ (πΉβ€˜π‘›) = (πΉβ€˜π‘˜)) β†’ 𝑛 = π‘˜)
4340, 42syl6bi 163 . . . . . . . 8 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ (({𝑛} Γ— (πΉβ€˜π‘›)) = ({π‘˜} Γ— (πΉβ€˜π‘˜)) β†’ 𝑛 = π‘˜))
4430, 43sylbid 150 . . . . . . 7 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ ((π΄β€˜π‘›) = ({π‘˜} Γ— (πΉβ€˜π‘˜)) β†’ 𝑛 = π‘˜))
4525, 44sylbid 150 . . . . . 6 ((πœ‘ ∧ (𝑛 ∈ Ο‰ ∧ π‘˜ ∈ Ο‰)) β†’ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜))
4645ralrimivva 2557 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ βˆ€π‘˜ ∈ Ο‰ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜))
47 dff13 5759 . . . . 5 (𝐴:ω–1-1β†’V ↔ (𝐴:Ο‰βŸΆV ∧ βˆ€π‘› ∈ Ο‰ βˆ€π‘˜ ∈ Ο‰ ((π΄β€˜π‘›) = (π΄β€˜π‘˜) β†’ 𝑛 = π‘˜)))
4811, 46, 47sylanbrc 417 . . . 4 (πœ‘ β†’ 𝐴:ω–1-1β†’V)
49 f1f1orn 5464 . . . . 5 (𝐴:ω–1-1β†’V β†’ 𝐴:ω–1-1-ontoβ†’ran 𝐴)
50 omex 4586 . . . . . 6 Ο‰ ∈ V
5150f1oen 6749 . . . . 5 (𝐴:ω–1-1-ontoβ†’ran 𝐴 β†’ Ο‰ β‰ˆ ran 𝐴)
52 ensym 6771 . . . . 5 (Ο‰ β‰ˆ ran 𝐴 β†’ ran 𝐴 β‰ˆ Ο‰)
5349, 51, 523syl 17 . . . 4 (𝐴:ω–1-1β†’V β†’ ran 𝐴 β‰ˆ Ο‰)
5448, 53syl 14 . . 3 (πœ‘ β†’ ran 𝐴 β‰ˆ Ο‰)
559ralrimiva 2548 . . . . . . . . 9 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ ({𝑛} Γ— (πΉβ€˜π‘›)) ∈ V)
5610fnmpt 5334 . . . . . . . . 9 (βˆ€π‘› ∈ Ο‰ ({𝑛} Γ— (πΉβ€˜π‘›)) ∈ V β†’ 𝐴 Fn Ο‰)
5755, 56syl 14 . . . . . . . 8 (πœ‘ β†’ 𝐴 Fn Ο‰)
5857adantr 276 . . . . . . 7 ((πœ‘ ∧ 𝑧 ∈ ran 𝐴) β†’ 𝐴 Fn Ο‰)
59 fnfun 5305 . . . . . . 7 (𝐴 Fn Ο‰ β†’ Fun 𝐴)
6058, 59syl 14 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ ran 𝐴) β†’ Fun 𝐴)
61 simpr 110 . . . . . 6 ((πœ‘ ∧ 𝑧 ∈ ran 𝐴) β†’ 𝑧 ∈ ran 𝐴)
62 elrnrexdm 5647 . . . . . 6 (Fun 𝐴 β†’ (𝑧 ∈ ran 𝐴 β†’ βˆƒπ‘› ∈ dom 𝐴 𝑧 = (π΄β€˜π‘›)))
6360, 61, 62sylc 62 . . . . 5 ((πœ‘ ∧ 𝑧 ∈ ran 𝐴) β†’ βˆƒπ‘› ∈ dom 𝐴 𝑧 = (π΄β€˜π‘›))
64 simpll 527 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ πœ‘)
65 simprl 529 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ 𝑛 ∈ dom 𝐴)
66 fndm 5307 . . . . . . . . 9 (𝐴 Fn Ο‰ β†’ dom 𝐴 = Ο‰)
6764, 57, 663syl 17 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ dom 𝐴 = Ο‰)
6865, 67eleqtrd 2254 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ 𝑛 ∈ Ο‰)
6935adantr 276 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ βˆ€π‘₯ ∈ Ο‰ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘₯))
7034, 69, 26rspcdva 2844 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘›))
71 eleq1 2238 . . . . . . . . . . 11 (𝑀 = π‘Ž β†’ (𝑀 ∈ (πΉβ€˜π‘›) ↔ π‘Ž ∈ (πΉβ€˜π‘›)))
7271cbvexv 1916 . . . . . . . . . 10 (βˆƒπ‘€ 𝑀 ∈ (πΉβ€˜π‘›) ↔ βˆƒπ‘Ž π‘Ž ∈ (πΉβ€˜π‘›))
7370, 72sylib 122 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ βˆƒπ‘Ž π‘Ž ∈ (πΉβ€˜π‘›))
74 vsnid 3621 . . . . . . . . . . 11 𝑛 ∈ {𝑛}
75 simpr 110 . . . . . . . . . . 11 (((πœ‘ ∧ 𝑛 ∈ Ο‰) ∧ π‘Ž ∈ (πΉβ€˜π‘›)) β†’ π‘Ž ∈ (πΉβ€˜π‘›))
76 opelxpi 4652 . . . . . . . . . . 11 ((𝑛 ∈ {𝑛} ∧ π‘Ž ∈ (πΉβ€˜π‘›)) β†’ βŸ¨π‘›, π‘ŽβŸ© ∈ ({𝑛} Γ— (πΉβ€˜π‘›)))
7774, 75, 76sylancr 414 . . . . . . . . . 10 (((πœ‘ ∧ 𝑛 ∈ Ο‰) ∧ π‘Ž ∈ (πΉβ€˜π‘›)) β†’ βŸ¨π‘›, π‘ŽβŸ© ∈ ({𝑛} Γ— (πΉβ€˜π‘›)))
78 eleq1 2238 . . . . . . . . . . 11 (𝑀 = βŸ¨π‘›, π‘ŽβŸ© β†’ (𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›)) ↔ βŸ¨π‘›, π‘ŽβŸ© ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
7978spcegv 2823 . . . . . . . . . 10 (βŸ¨π‘›, π‘ŽβŸ© ∈ ({𝑛} Γ— (πΉβ€˜π‘›)) β†’ (βŸ¨π‘›, π‘ŽβŸ© ∈ ({𝑛} Γ— (πΉβ€˜π‘›)) β†’ βˆƒπ‘€ 𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
8077, 77, 79sylc 62 . . . . . . . . 9 (((πœ‘ ∧ 𝑛 ∈ Ο‰) ∧ π‘Ž ∈ (πΉβ€˜π‘›)) β†’ βˆƒπ‘€ 𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›)))
8173, 80exlimddv 1896 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ βˆƒπ‘€ 𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›)))
8228eleq2d 2245 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (𝑀 ∈ (π΄β€˜π‘›) ↔ 𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
8382exbidv 1823 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (βˆƒπ‘€ 𝑀 ∈ (π΄β€˜π‘›) ↔ βˆƒπ‘€ 𝑀 ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
8481, 83mpbird 167 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ βˆƒπ‘€ 𝑀 ∈ (π΄β€˜π‘›))
8564, 68, 84syl2anc 411 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ βˆƒπ‘€ 𝑀 ∈ (π΄β€˜π‘›))
86 simprr 531 . . . . . . . 8 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ 𝑧 = (π΄β€˜π‘›))
8786eleq2d 2245 . . . . . . 7 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ (𝑀 ∈ 𝑧 ↔ 𝑀 ∈ (π΄β€˜π‘›)))
8887exbidv 1823 . . . . . 6 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ (βˆƒπ‘€ 𝑀 ∈ 𝑧 ↔ βˆƒπ‘€ 𝑀 ∈ (π΄β€˜π‘›)))
8985, 88mpbird 167 . . . . 5 (((πœ‘ ∧ 𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴 ∧ 𝑧 = (π΄β€˜π‘›))) β†’ βˆƒπ‘€ 𝑀 ∈ 𝑧)
9063, 89rexlimddv 2597 . . . 4 ((πœ‘ ∧ 𝑧 ∈ ran 𝐴) β†’ βˆƒπ‘€ 𝑀 ∈ 𝑧)
9190ralrimiva 2548 . . 3 (πœ‘ β†’ βˆ€π‘§ ∈ ran π΄βˆƒπ‘€ 𝑀 ∈ 𝑧)
921, 54, 91ccfunen 7238 . 2 (πœ‘ β†’ βˆƒπ‘“(𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧))
93 vex 2738 . . . . . . . 8 𝑓 ∈ V
94 funfvex 5524 . . . . . . . . . 10 ((Fun 𝐴 ∧ 𝑛 ∈ dom 𝐴) β†’ (π΄β€˜π‘›) ∈ V)
9594funfni 5308 . . . . . . . . 9 ((𝐴 Fn Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ V)
9657, 95sylan 283 . . . . . . . 8 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ V)
97 fvexg 5526 . . . . . . . 8 ((𝑓 ∈ V ∧ (π΄β€˜π‘›) ∈ V) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ V)
9893, 96, 97sylancr 414 . . . . . . 7 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ V)
99 2ndexg 6159 . . . . . . 7 ((π‘“β€˜(π΄β€˜π‘›)) ∈ V β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V)
10098, 99syl 14 . . . . . 6 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V)
101100ralrimiva 2548 . . . . 5 (πœ‘ β†’ βˆ€π‘› ∈ Ο‰ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V)
102 cc2lem.g . . . . . 6 𝐺 = (𝑛 ∈ Ο‰ ↦ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
103102fnmpt 5334 . . . . 5 (βˆ€π‘› ∈ Ο‰ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ V β†’ 𝐺 Fn Ο‰)
104101, 103syl 14 . . . 4 (πœ‘ β†’ 𝐺 Fn Ο‰)
105104adantr 276 . . 3 ((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) β†’ 𝐺 Fn Ο‰)
106 simpr 110 . . . . . 6 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ 𝑛 ∈ Ο‰)
107 fveq2 5507 . . . . . . . . . 10 (𝑧 = (π΄β€˜π‘›) β†’ (π‘“β€˜π‘§) = (π‘“β€˜(π΄β€˜π‘›)))
108 id 19 . . . . . . . . . 10 (𝑧 = (π΄β€˜π‘›) β†’ 𝑧 = (π΄β€˜π‘›))
109107, 108eleq12d 2246 . . . . . . . . 9 (𝑧 = (π΄β€˜π‘›) β†’ ((π‘“β€˜π‘§) ∈ 𝑧 ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›)))
110 simplrr 536 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)
111 fnfvelrn 5640 . . . . . . . . . . 11 ((𝐴 Fn Ο‰ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ ran 𝐴)
11257, 111sylan 283 . . . . . . . . . 10 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ ran 𝐴)
113112adantlr 477 . . . . . . . . 9 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (π΄β€˜π‘›) ∈ ran 𝐴)
114109, 110, 113rspcdva 2844 . . . . . . . 8 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›))
11528eleq2d 2245 . . . . . . . . 9 ((πœ‘ ∧ 𝑛 ∈ Ο‰) β†’ ((π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›) ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
116115adantlr 477 . . . . . . . 8 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ ((π‘“β€˜(π΄β€˜π‘›)) ∈ (π΄β€˜π‘›) ↔ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΉβ€˜π‘›))))
117114, 116mpbid 147 . . . . . . 7 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΉβ€˜π‘›)))
118 xp2nd 6157 . . . . . . 7 ((π‘“β€˜(π΄β€˜π‘›)) ∈ ({𝑛} Γ— (πΉβ€˜π‘›)) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΉβ€˜π‘›))
119117, 118syl 14 . . . . . 6 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΉβ€˜π‘›))
120102fvmpt2 5591 . . . . . 6 ((𝑛 ∈ Ο‰ ∧ (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))) ∈ (πΉβ€˜π‘›)) β†’ (πΊβ€˜π‘›) = (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
121106, 119, 120syl2anc 411 . . . . 5 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (πΊβ€˜π‘›) = (2nd β€˜(π‘“β€˜(π΄β€˜π‘›))))
122121, 119eqeltrd 2252 . . . 4 (((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) ∧ 𝑛 ∈ Ο‰) β†’ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))
123122ralrimiva 2548 . . 3 ((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) β†’ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))
12450a1i 9 . . . . . 6 (πœ‘ β†’ Ο‰ ∈ V)
125 fnex 5730 . . . . . 6 ((𝐺 Fn Ο‰ ∧ Ο‰ ∈ V) β†’ 𝐺 ∈ V)
126104, 124, 125syl2anc 411 . . . . 5 (πœ‘ β†’ 𝐺 ∈ V)
127 fneq1 5296 . . . . . . 7 (𝑔 = 𝐺 β†’ (𝑔 Fn Ο‰ ↔ 𝐺 Fn Ο‰))
128 fveq1 5506 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (π‘”β€˜π‘›) = (πΊβ€˜π‘›))
129128eleq1d 2244 . . . . . . . 8 (𝑔 = 𝐺 β†’ ((π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))
130129ralbidv 2475 . . . . . . 7 (𝑔 = 𝐺 β†’ (βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›) ↔ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)))
131127, 130anbi12d 473 . . . . . 6 (𝑔 = 𝐺 β†’ ((𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)) ↔ (𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›))))
132131spcegv 2823 . . . . 5 (𝐺 ∈ V β†’ ((𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))))
133126, 132syl 14 . . . 4 (πœ‘ β†’ ((𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))))
134133adantr 276 . . 3 ((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) β†’ ((𝐺 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (πΊβ€˜π‘›) ∈ (πΉβ€˜π‘›)) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›))))
135105, 123, 134mp2and 433 . 2 ((πœ‘ ∧ (𝑓 Fn ran 𝐴 ∧ βˆ€π‘§ ∈ ran 𝐴(π‘“β€˜π‘§) ∈ 𝑧)) β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)))
13692, 135exlimddv 1896 1 (πœ‘ β†’ βˆƒπ‘”(𝑔 Fn Ο‰ ∧ βˆ€π‘› ∈ Ο‰ (π‘”β€˜π‘›) ∈ (πΉβ€˜π‘›)))
Colors of variables: wff set class
Syntax hints:   β†’ wi 4   ∧ wa 104   ↔ wb 105   = wceq 1353  βˆƒwex 1490   ∈ wcel 2146  βˆ€wral 2453  βˆƒwrex 2454  Vcvv 2735  {csn 3589  βŸ¨cop 3592   class class class wbr 3998   ↦ cmpt 4059  Ο‰com 4583   Γ— cxp 4618  dom cdm 4620  ran crn 4621  Fun wfun 5202   Fn wfn 5203  βŸΆwf 5204  β€“1-1β†’wf1 5205  β€“1-1-ontoβ†’wf1o 5207  β€˜cfv 5208  2nd c2nd 6130   β‰ˆ cen 6728  CCHOICEwacc 7236
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-13 2148  ax-14 2149  ax-ext 2157  ax-coll 4113  ax-sep 4116  ax-pow 4169  ax-pr 4203  ax-un 4427  ax-iinf 4581
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1459  df-sb 1761  df-eu 2027  df-mo 2028  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-rex 2459  df-reu 2460  df-rab 2462  df-v 2737  df-sbc 2961  df-csb 3056  df-un 3131  df-in 3133  df-ss 3140  df-pw 3574  df-sn 3595  df-pr 3596  df-op 3598  df-uni 3806  df-int 3841  df-iun 3884  df-br 3999  df-opab 4060  df-mpt 4061  df-id 4287  df-iom 4584  df-xp 4626  df-rel 4627  df-cnv 4628  df-co 4629  df-dm 4630  df-rn 4631  df-res 4632  df-ima 4633  df-iota 5170  df-fun 5210  df-fn 5211  df-f 5212  df-f1 5213  df-fo 5214  df-f1o 5215  df-fv 5216  df-2nd 6132  df-er 6525  df-en 6731  df-cc 7237
This theorem is referenced by:  cc2  7241
  Copyright terms: Public domain W3C validator