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

Theorem cc2lem 7256
Description: Lemma for cc2 7257. (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 2740 . . . . . . . 8 𝑛 ∈ V
32snex 4182 . . . . . . 7 {𝑛} ∈ V
4 cc2.a . . . . . . . 8 (𝜑𝐹 Fn ω)
5 funfvex 5528 . . . . . . . . 9 ((Fun 𝐹𝑛 ∈ dom 𝐹) → (𝐹𝑛) ∈ V)
65funfni 5312 . . . . . . . 8 ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹𝑛) ∈ V)
74, 6sylan 283 . . . . . . 7 ((𝜑𝑛 ∈ ω) → (𝐹𝑛) ∈ V)
8 xpexg 4737 . . . . . . 7 (({𝑛} ∈ V ∧ (𝐹𝑛) ∈ V) → ({𝑛} × (𝐹𝑛)) ∈ V)
93, 7, 8sylancr 414 . . . . . 6 ((𝜑𝑛 ∈ ω) → ({𝑛} × (𝐹𝑛)) ∈ V)
10 cc2lem.a . . . . . 6 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹𝑛)))
119, 10fmptd 5666 . . . . 5 (𝜑𝐴:ω⟶V)
12 sneq 3602 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑛} = {𝑘})
13 fveq2 5511 . . . . . . . . . 10 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1412, 13xpeq12d 4648 . . . . . . . . 9 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
15 simprr 531 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16 vex 2740 . . . . . . . . . . 11 𝑘 ∈ V
1716snex 4182 . . . . . . . . . 10 {𝑘} ∈ V
184adantr 276 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19 funfvex 5528 . . . . . . . . . . . 12 ((Fun 𝐹𝑘 ∈ dom 𝐹) → (𝐹𝑘) ∈ V)
2019funfni 5312 . . . . . . . . . . 11 ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹𝑘) ∈ V)
2118, 15, 20syl2anc 411 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹𝑘) ∈ V)
22 xpexg 4737 . . . . . . . . . 10 (({𝑘} ∈ V ∧ (𝐹𝑘) ∈ V) → ({𝑘} × (𝐹𝑘)) ∈ V)
2317, 21, 22sylancr 414 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹𝑘)) ∈ V)
2410, 14, 15, 23fvmptd3 5605 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴𝑘) = ({𝑘} × (𝐹𝑘)))
2524eqeq2d 2189 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = (𝐴𝑘) ↔ (𝐴𝑛) = ({𝑘} × (𝐹𝑘))))
26 simpr 110 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ω) → 𝑛 ∈ ω)
2710fvmpt2 5595 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹𝑛)) ∈ V) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
2826, 9, 27syl2anc 411 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
2928adantrr 479 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
3029eqeq1d 2186 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘))))
312snm 3711 . . . . . . . . . 10 𝑤 𝑤 ∈ {𝑛}
32 fveq2 5511 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝐹𝑥) = (𝐹𝑛))
3332eleq2d 2247 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝑤 ∈ (𝐹𝑥) ↔ 𝑤 ∈ (𝐹𝑛)))
3433exbidv 1825 . . . . . . . . . . 11 (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹𝑛)))
35 cc2.m . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
3635adantr 276 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
37 simprl 529 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
3834, 36, 37rspcdva 2846 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹𝑛))
39 xp11m 5063 . . . . . . . . . 10 ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹𝑛)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘))))
4031, 38, 39sylancr 414 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘))))
412sneqr 3758 . . . . . . . . . 10 ({𝑛} = {𝑘} → 𝑛 = 𝑘)
4241adantr 276 . . . . . . . . 9 (({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘)) → 𝑛 = 𝑘)
4340, 42syl6bi 163 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) → 𝑛 = 𝑘))
4430, 43sylbid 150 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = ({𝑘} × (𝐹𝑘)) → 𝑛 = 𝑘))
4525, 44sylbid 150 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘))
4645ralrimivva 2559 . . . . 5 (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘))
47 dff13 5763 . . . . 5 (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘)))
4811, 46, 47sylanbrc 417 . . . 4 (𝜑𝐴:ω–1-1→V)
49 f1f1orn 5468 . . . . 5 (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50 omex 4589 . . . . . 6 ω ∈ V
5150f1oen 6753 . . . . 5 (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52 ensym 6775 . . . . 5 (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
5349, 51, 523syl 17 . . . 4 (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
5448, 53syl 14 . . 3 (𝜑 → ran 𝐴 ≈ ω)
559ralrimiva 2550 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹𝑛)) ∈ V)
5610fnmpt 5338 . . . . . . . . 9 (∀𝑛 ∈ ω ({𝑛} × (𝐹𝑛)) ∈ V → 𝐴 Fn ω)
5755, 56syl 14 . . . . . . . 8 (𝜑𝐴 Fn ω)
5857adantr 276 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59 fnfun 5309 . . . . . . 7 (𝐴 Fn ω → Fun 𝐴)
6058, 59syl 14 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐴) → Fun 𝐴)
61 simpr 110 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62 elrnrexdm 5651 . . . . . 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 5311 . . . . . . . . 9 (𝐴 Fn ω → dom 𝐴 = ω)
6764, 57, 663syl 17 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → dom 𝐴 = ω)
6865, 67eleqtrd 2256 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝑛 ∈ ω)
6935adantr 276 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
7034, 69, 26rspcdva 2846 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹𝑛))
71 eleq1 2240 . . . . . . . . . . 11 (𝑤 = 𝑎 → (𝑤 ∈ (𝐹𝑛) ↔ 𝑎 ∈ (𝐹𝑛)))
7271cbvexv 1918 . . . . . . . . . 10 (∃𝑤 𝑤 ∈ (𝐹𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹𝑛))
7370, 72sylib 122 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹𝑛))
74 vsnid 3623 . . . . . . . . . . 11 𝑛 ∈ {𝑛}
75 simpr 110 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → 𝑎 ∈ (𝐹𝑛))
76 opelxpi 4655 . . . . . . . . . . 11 ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)))
7774, 75, 76sylancr 414 . . . . . . . . . 10 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)))
78 eleq1 2240 . . . . . . . . . . 11 (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛))))
7978spcegv 2825 . . . . . . . . . 10 (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8077, 77, 79sylc 62 . . . . . . . . 9 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛)))
8173, 80exlimddv 1898 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛)))
8228eleq2d 2247 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → (𝑤 ∈ (𝐴𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8382exbidv 1825 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8481, 83mpbird 167 . . . . . . 7 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴𝑛))
8564, 68, 84syl2anc 411 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → ∃𝑤 𝑤 ∈ (𝐴𝑛))
86 simprr 531 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝑧 = (𝐴𝑛))
8786eleq2d 2247 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → (𝑤𝑧𝑤 ∈ (𝐴𝑛)))
8887exbidv 1825 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → (∃𝑤 𝑤𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴𝑛)))
8985, 88mpbird 167 . . . . 5 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → ∃𝑤 𝑤𝑧)
9063, 89rexlimddv 2599 . . . 4 ((𝜑𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤𝑧)
9190ralrimiva 2550 . . 3 (𝜑 → ∀𝑧 ∈ ran 𝐴𝑤 𝑤𝑧)
921, 54, 91ccfunen 7254 . 2 (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧))
93 vex 2740 . . . . . . . 8 𝑓 ∈ V
94 funfvex 5528 . . . . . . . . . 10 ((Fun 𝐴𝑛 ∈ dom 𝐴) → (𝐴𝑛) ∈ V)
9594funfni 5312 . . . . . . . . 9 ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ V)
9657, 95sylan 283 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) ∈ V)
97 fvexg 5530 . . . . . . . 8 ((𝑓 ∈ V ∧ (𝐴𝑛) ∈ V) → (𝑓‘(𝐴𝑛)) ∈ V)
9893, 96, 97sylancr 414 . . . . . . 7 ((𝜑𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ V)
99 2ndexg 6163 . . . . . . 7 ((𝑓‘(𝐴𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
10098, 99syl 14 . . . . . 6 ((𝜑𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
101100ralrimiva 2550 . . . . 5 (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
102 cc2lem.g . . . . . 6 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴𝑛))))
103102fnmpt 5338 . . . . 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 5511 . . . . . . . . . 10 (𝑧 = (𝐴𝑛) → (𝑓𝑧) = (𝑓‘(𝐴𝑛)))
108 id 19 . . . . . . . . . 10 (𝑧 = (𝐴𝑛) → 𝑧 = (𝐴𝑛))
109107, 108eleq12d 2248 . . . . . . . . 9 (𝑧 = (𝐴𝑛) → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛)))
110 simplrr 536 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)
111 fnfvelrn 5644 . . . . . . . . . . 11 ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
11257, 111sylan 283 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
113112adantlr 477 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
114109, 110, 113rspcdva 2846 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛))
11528eleq2d 2247 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → ((𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛) ↔ (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛))))
116115adantlr 477 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛) ↔ (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛))))
117114, 116mpbid 147 . . . . . . 7 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛)))
118 xp2nd 6161 . . . . . . 7 ((𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛)) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛))
119117, 118syl 14 . . . . . 6 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛))
120102fvmpt2 5595 . . . . . 6 ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛)) → (𝐺𝑛) = (2nd ‘(𝑓‘(𝐴𝑛))))
121106, 119, 120syl2anc 411 . . . . 5 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺𝑛) = (2nd ‘(𝑓‘(𝐴𝑛))))
122121, 119eqeltrd 2254 . . . 4 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺𝑛) ∈ (𝐹𝑛))
123122ralrimiva 2550 . . 3 ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛))
12450a1i 9 . . . . . 6 (𝜑 → ω ∈ V)
125 fnex 5734 . . . . . 6 ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126104, 124, 125syl2anc 411 . . . . 5 (𝜑𝐺 ∈ V)
127 fneq1 5300 . . . . . . 7 (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128 fveq1 5510 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔𝑛) = (𝐺𝑛))
129128eleq1d 2246 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔𝑛) ∈ (𝐹𝑛) ↔ (𝐺𝑛) ∈ (𝐹𝑛)))
130129ralbidv 2477 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛) ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛)))
131127, 130anbi12d 473 . . . . . 6 (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛))))
132131spcegv 2825 . . . . 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 1898 1 (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wex 1492  wcel 2148  wral 2455  wrex 2456  Vcvv 2737  {csn 3591  cop 3594   class class class wbr 4000  cmpt 4061  ωcom 4586   × cxp 4621  dom cdm 4623  ran crn 4624  Fun wfun 5206   Fn wfn 5207  wf 5208  1-1wf1 5209  1-1-ontowf1o 5211  cfv 5212  2nd c2nd 6134  cen 6732  CCHOICEwacc 7252
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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4115  ax-sep 4118  ax-pow 4171  ax-pr 4206  ax-un 4430  ax-iinf 4584
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  df-pw 3576  df-sn 3597  df-pr 3598  df-op 3600  df-uni 3808  df-int 3843  df-iun 3886  df-br 4001  df-opab 4062  df-mpt 4063  df-id 4290  df-iom 4587  df-xp 4629  df-rel 4630  df-cnv 4631  df-co 4632  df-dm 4633  df-rn 4634  df-res 4635  df-ima 4636  df-iota 5174  df-fun 5214  df-fn 5215  df-f 5216  df-f1 5217  df-fo 5218  df-f1o 5219  df-fv 5220  df-2nd 6136  df-er 6529  df-en 6735  df-cc 7253
This theorem is referenced by:  cc2  7257
  Copyright terms: Public domain W3C validator