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

Theorem cc2lem 7086
 Description: Lemma for cc2 7087. (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 2689 . . . . . . . 8 𝑛 ∈ V
32snex 4109 . . . . . . 7 {𝑛} ∈ V
4 cc2.a . . . . . . . 8 (𝜑𝐹 Fn ω)
5 funfvex 5438 . . . . . . . . 9 ((Fun 𝐹𝑛 ∈ dom 𝐹) → (𝐹𝑛) ∈ V)
65funfni 5223 . . . . . . . 8 ((𝐹 Fn ω ∧ 𝑛 ∈ ω) → (𝐹𝑛) ∈ V)
74, 6sylan 281 . . . . . . 7 ((𝜑𝑛 ∈ ω) → (𝐹𝑛) ∈ V)
8 xpexg 4653 . . . . . . 7 (({𝑛} ∈ V ∧ (𝐹𝑛) ∈ V) → ({𝑛} × (𝐹𝑛)) ∈ V)
93, 7, 8sylancr 410 . . . . . 6 ((𝜑𝑛 ∈ ω) → ({𝑛} × (𝐹𝑛)) ∈ V)
10 cc2lem.a . . . . . 6 𝐴 = (𝑛 ∈ ω ↦ ({𝑛} × (𝐹𝑛)))
119, 10fmptd 5574 . . . . 5 (𝜑𝐴:ω⟶V)
12 sneq 3538 . . . . . . . . . 10 (𝑛 = 𝑘 → {𝑛} = {𝑘})
13 fveq2 5421 . . . . . . . . . 10 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
1412, 13xpeq12d 4564 . . . . . . . . 9 (𝑛 = 𝑘 → ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)))
15 simprr 521 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑘 ∈ ω)
16 vex 2689 . . . . . . . . . . 11 𝑘 ∈ V
1716snex 4109 . . . . . . . . . 10 {𝑘} ∈ V
184adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝐹 Fn ω)
19 funfvex 5438 . . . . . . . . . . . 12 ((Fun 𝐹𝑘 ∈ dom 𝐹) → (𝐹𝑘) ∈ V)
2019funfni 5223 . . . . . . . . . . 11 ((𝐹 Fn ω ∧ 𝑘 ∈ ω) → (𝐹𝑘) ∈ V)
2118, 15, 20syl2anc 408 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐹𝑘) ∈ V)
22 xpexg 4653 . . . . . . . . . 10 (({𝑘} ∈ V ∧ (𝐹𝑘) ∈ V) → ({𝑘} × (𝐹𝑘)) ∈ V)
2317, 21, 22sylancr 410 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ({𝑘} × (𝐹𝑘)) ∈ V)
2410, 14, 15, 23fvmptd3 5514 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴𝑘) = ({𝑘} × (𝐹𝑘)))
2524eqeq2d 2151 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = (𝐴𝑘) ↔ (𝐴𝑛) = ({𝑘} × (𝐹𝑘))))
26 simpr 109 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ω) → 𝑛 ∈ ω)
2710fvmpt2 5504 . . . . . . . . . . 11 ((𝑛 ∈ ω ∧ ({𝑛} × (𝐹𝑛)) ∈ V) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
2826, 9, 27syl2anc 408 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
2928adantrr 470 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (𝐴𝑛) = ({𝑛} × (𝐹𝑛)))
3029eqeq1d 2148 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘))))
312snm 3643 . . . . . . . . . 10 𝑤 𝑤 ∈ {𝑛}
32 fveq2 5421 . . . . . . . . . . . . 13 (𝑥 = 𝑛 → (𝐹𝑥) = (𝐹𝑛))
3332eleq2d 2209 . . . . . . . . . . . 12 (𝑥 = 𝑛 → (𝑤 ∈ (𝐹𝑥) ↔ 𝑤 ∈ (𝐹𝑛)))
3433exbidv 1797 . . . . . . . . . . 11 (𝑥 = 𝑛 → (∃𝑤 𝑤 ∈ (𝐹𝑥) ↔ ∃𝑤 𝑤 ∈ (𝐹𝑛)))
35 cc2.m . . . . . . . . . . . 12 (𝜑 → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
3635adantr 274 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
37 simprl 520 . . . . . . . . . . 11 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → 𝑛 ∈ ω)
3834, 36, 37rspcdva 2794 . . . . . . . . . 10 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ∃𝑤 𝑤 ∈ (𝐹𝑛))
39 xp11m 4977 . . . . . . . . . 10 ((∃𝑤 𝑤 ∈ {𝑛} ∧ ∃𝑤 𝑤 ∈ (𝐹𝑛)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘))))
4031, 38, 39sylancr 410 . . . . . . . . 9 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) ↔ ({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘))))
412sneqr 3687 . . . . . . . . . 10 ({𝑛} = {𝑘} → 𝑛 = 𝑘)
4241adantr 274 . . . . . . . . 9 (({𝑛} = {𝑘} ∧ (𝐹𝑛) = (𝐹𝑘)) → 𝑛 = 𝑘)
4340, 42syl6bi 162 . . . . . . . 8 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → (({𝑛} × (𝐹𝑛)) = ({𝑘} × (𝐹𝑘)) → 𝑛 = 𝑘))
4430, 43sylbid 149 . . . . . . 7 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = ({𝑘} × (𝐹𝑘)) → 𝑛 = 𝑘))
4525, 44sylbid 149 . . . . . 6 ((𝜑 ∧ (𝑛 ∈ ω ∧ 𝑘 ∈ ω)) → ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘))
4645ralrimivva 2514 . . . . 5 (𝜑 → ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘))
47 dff13 5669 . . . . 5 (𝐴:ω–1-1→V ↔ (𝐴:ω⟶V ∧ ∀𝑛 ∈ ω ∀𝑘 ∈ ω ((𝐴𝑛) = (𝐴𝑘) → 𝑛 = 𝑘)))
4811, 46, 47sylanbrc 413 . . . 4 (𝜑𝐴:ω–1-1→V)
49 f1f1orn 5378 . . . . 5 (𝐴:ω–1-1→V → 𝐴:ω–1-1-onto→ran 𝐴)
50 omex 4507 . . . . . 6 ω ∈ V
5150f1oen 6653 . . . . 5 (𝐴:ω–1-1-onto→ran 𝐴 → ω ≈ ran 𝐴)
52 ensym 6675 . . . . 5 (ω ≈ ran 𝐴 → ran 𝐴 ≈ ω)
5349, 51, 523syl 17 . . . 4 (𝐴:ω–1-1→V → ran 𝐴 ≈ ω)
5448, 53syl 14 . . 3 (𝜑 → ran 𝐴 ≈ ω)
559ralrimiva 2505 . . . . . . . . 9 (𝜑 → ∀𝑛 ∈ ω ({𝑛} × (𝐹𝑛)) ∈ V)
5610fnmpt 5249 . . . . . . . . 9 (∀𝑛 ∈ ω ({𝑛} × (𝐹𝑛)) ∈ V → 𝐴 Fn ω)
5755, 56syl 14 . . . . . . . 8 (𝜑𝐴 Fn ω)
5857adantr 274 . . . . . . 7 ((𝜑𝑧 ∈ ran 𝐴) → 𝐴 Fn ω)
59 fnfun 5220 . . . . . . 7 (𝐴 Fn ω → Fun 𝐴)
6058, 59syl 14 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐴) → Fun 𝐴)
61 simpr 109 . . . . . 6 ((𝜑𝑧 ∈ ran 𝐴) → 𝑧 ∈ ran 𝐴)
62 elrnrexdm 5559 . . . . . 6 (Fun 𝐴 → (𝑧 ∈ ran 𝐴 → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴𝑛)))
6360, 61, 62sylc 62 . . . . 5 ((𝜑𝑧 ∈ ran 𝐴) → ∃𝑛 ∈ dom 𝐴 𝑧 = (𝐴𝑛))
64 simpll 518 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝜑)
65 simprl 520 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝑛 ∈ dom 𝐴)
66 fndm 5222 . . . . . . . . 9 (𝐴 Fn ω → dom 𝐴 = ω)
6764, 57, 663syl 17 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → dom 𝐴 = ω)
6865, 67eleqtrd 2218 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝑛 ∈ ω)
6935adantr 274 . . . . . . . . . . 11 ((𝜑𝑛 ∈ ω) → ∀𝑥 ∈ ω ∃𝑤 𝑤 ∈ (𝐹𝑥))
7034, 69, 26rspcdva 2794 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐹𝑛))
71 eleq1 2202 . . . . . . . . . . 11 (𝑤 = 𝑎 → (𝑤 ∈ (𝐹𝑛) ↔ 𝑎 ∈ (𝐹𝑛)))
7271cbvexv 1890 . . . . . . . . . 10 (∃𝑤 𝑤 ∈ (𝐹𝑛) ↔ ∃𝑎 𝑎 ∈ (𝐹𝑛))
7370, 72sylib 121 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → ∃𝑎 𝑎 ∈ (𝐹𝑛))
74 vsnid 3557 . . . . . . . . . . 11 𝑛 ∈ {𝑛}
75 simpr 109 . . . . . . . . . . 11 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → 𝑎 ∈ (𝐹𝑛))
76 opelxpi 4571 . . . . . . . . . . 11 ((𝑛 ∈ {𝑛} ∧ 𝑎 ∈ (𝐹𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)))
7774, 75, 76sylancr 410 . . . . . . . . . 10 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)))
78 eleq1 2202 . . . . . . . . . . 11 (𝑤 = ⟨𝑛, 𝑎⟩ → (𝑤 ∈ ({𝑛} × (𝐹𝑛)) ↔ ⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛))))
7978spcegv 2774 . . . . . . . . . 10 (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)) → (⟨𝑛, 𝑎⟩ ∈ ({𝑛} × (𝐹𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8077, 77, 79sylc 62 . . . . . . . . 9 (((𝜑𝑛 ∈ ω) ∧ 𝑎 ∈ (𝐹𝑛)) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛)))
8173, 80exlimddv 1870 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛)))
8228eleq2d 2209 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → (𝑤 ∈ (𝐴𝑛) ↔ 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8382exbidv 1797 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → (∃𝑤 𝑤 ∈ (𝐴𝑛) ↔ ∃𝑤 𝑤 ∈ ({𝑛} × (𝐹𝑛))))
8481, 83mpbird 166 . . . . . . 7 ((𝜑𝑛 ∈ ω) → ∃𝑤 𝑤 ∈ (𝐴𝑛))
8564, 68, 84syl2anc 408 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → ∃𝑤 𝑤 ∈ (𝐴𝑛))
86 simprr 521 . . . . . . . 8 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → 𝑧 = (𝐴𝑛))
8786eleq2d 2209 . . . . . . 7 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → (𝑤𝑧𝑤 ∈ (𝐴𝑛)))
8887exbidv 1797 . . . . . 6 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → (∃𝑤 𝑤𝑧 ↔ ∃𝑤 𝑤 ∈ (𝐴𝑛)))
8985, 88mpbird 166 . . . . 5 (((𝜑𝑧 ∈ ran 𝐴) ∧ (𝑛 ∈ dom 𝐴𝑧 = (𝐴𝑛))) → ∃𝑤 𝑤𝑧)
9063, 89rexlimddv 2554 . . . 4 ((𝜑𝑧 ∈ ran 𝐴) → ∃𝑤 𝑤𝑧)
9190ralrimiva 2505 . . 3 (𝜑 → ∀𝑧 ∈ ran 𝐴𝑤 𝑤𝑧)
921, 54, 91ccfunen 7084 . 2 (𝜑 → ∃𝑓(𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧))
93 vex 2689 . . . . . . . 8 𝑓 ∈ V
94 funfvex 5438 . . . . . . . . . 10 ((Fun 𝐴𝑛 ∈ dom 𝐴) → (𝐴𝑛) ∈ V)
9594funfni 5223 . . . . . . . . 9 ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ V)
9657, 95sylan 281 . . . . . . . 8 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) ∈ V)
97 fvexg 5440 . . . . . . . 8 ((𝑓 ∈ V ∧ (𝐴𝑛) ∈ V) → (𝑓‘(𝐴𝑛)) ∈ V)
9893, 96, 97sylancr 410 . . . . . . 7 ((𝜑𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ V)
99 2ndexg 6066 . . . . . . 7 ((𝑓‘(𝐴𝑛)) ∈ V → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
10098, 99syl 14 . . . . . 6 ((𝜑𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
101100ralrimiva 2505 . . . . 5 (𝜑 → ∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V)
102 cc2lem.g . . . . . 6 𝐺 = (𝑛 ∈ ω ↦ (2nd ‘(𝑓‘(𝐴𝑛))))
103102fnmpt 5249 . . . . 5 (∀𝑛 ∈ ω (2nd ‘(𝑓‘(𝐴𝑛))) ∈ V → 𝐺 Fn ω)
104101, 103syl 14 . . . 4 (𝜑𝐺 Fn ω)
105104adantr 274 . . 3 ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) → 𝐺 Fn ω)
106 simpr 109 . . . . . 6 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → 𝑛 ∈ ω)
107 fveq2 5421 . . . . . . . . . 10 (𝑧 = (𝐴𝑛) → (𝑓𝑧) = (𝑓‘(𝐴𝑛)))
108 id 19 . . . . . . . . . 10 (𝑧 = (𝐴𝑛) → 𝑧 = (𝐴𝑛))
109107, 108eleq12d 2210 . . . . . . . . 9 (𝑧 = (𝐴𝑛) → ((𝑓𝑧) ∈ 𝑧 ↔ (𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛)))
110 simplrr 525 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)
111 fnfvelrn 5552 . . . . . . . . . . 11 ((𝐴 Fn ω ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
11257, 111sylan 281 . . . . . . . . . 10 ((𝜑𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
113112adantlr 468 . . . . . . . . 9 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐴𝑛) ∈ ran 𝐴)
114109, 110, 113rspcdva 2794 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛))
11528eleq2d 2209 . . . . . . . . 9 ((𝜑𝑛 ∈ ω) → ((𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛) ↔ (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛))))
116115adantlr 468 . . . . . . . 8 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → ((𝑓‘(𝐴𝑛)) ∈ (𝐴𝑛) ↔ (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛))))
117114, 116mpbid 146 . . . . . . 7 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛)))
118 xp2nd 6064 . . . . . . 7 ((𝑓‘(𝐴𝑛)) ∈ ({𝑛} × (𝐹𝑛)) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛))
119117, 118syl 14 . . . . . 6 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛))
120102fvmpt2 5504 . . . . . 6 ((𝑛 ∈ ω ∧ (2nd ‘(𝑓‘(𝐴𝑛))) ∈ (𝐹𝑛)) → (𝐺𝑛) = (2nd ‘(𝑓‘(𝐴𝑛))))
121106, 119, 120syl2anc 408 . . . . 5 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺𝑛) = (2nd ‘(𝑓‘(𝐴𝑛))))
122121, 119eqeltrd 2216 . . . 4 (((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) ∧ 𝑛 ∈ ω) → (𝐺𝑛) ∈ (𝐹𝑛))
123122ralrimiva 2505 . . 3 ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) → ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛))
12450a1i 9 . . . . . 6 (𝜑 → ω ∈ V)
125 fnex 5642 . . . . . 6 ((𝐺 Fn ω ∧ ω ∈ V) → 𝐺 ∈ V)
126104, 124, 125syl2anc 408 . . . . 5 (𝜑𝐺 ∈ V)
127 fneq1 5211 . . . . . . 7 (𝑔 = 𝐺 → (𝑔 Fn ω ↔ 𝐺 Fn ω))
128 fveq1 5420 . . . . . . . . 9 (𝑔 = 𝐺 → (𝑔𝑛) = (𝐺𝑛))
129128eleq1d 2208 . . . . . . . 8 (𝑔 = 𝐺 → ((𝑔𝑛) ∈ (𝐹𝑛) ↔ (𝐺𝑛) ∈ (𝐹𝑛)))
130129ralbidv 2437 . . . . . . 7 (𝑔 = 𝐺 → (∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛) ↔ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛)))
131127, 130anbi12d 464 . . . . . 6 (𝑔 = 𝐺 → ((𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)) ↔ (𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛))))
132131spcegv 2774 . . . . 5 (𝐺 ∈ V → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛))))
133126, 132syl 14 . . . 4 (𝜑 → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛))))
134133adantr 274 . . 3 ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) → ((𝐺 Fn ω ∧ ∀𝑛 ∈ ω (𝐺𝑛) ∈ (𝐹𝑛)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛))))
135105, 123, 134mp2and 429 . 2 ((𝜑 ∧ (𝑓 Fn ran 𝐴 ∧ ∀𝑧 ∈ ran 𝐴(𝑓𝑧) ∈ 𝑧)) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)))
13692, 135exlimddv 1870 1 (𝜑 → ∃𝑔(𝑔 Fn ω ∧ ∀𝑛 ∈ ω (𝑔𝑛) ∈ (𝐹𝑛)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  ∃wrex 2417  Vcvv 2686  {csn 3527  ⟨cop 3530   class class class wbr 3929   ↦ cmpt 3989  ωcom 4504   × cxp 4537  dom cdm 4539  ran crn 4540  Fun wfun 5117   Fn wfn 5118  ⟶wf 5119  –1-1→wf1 5120  –1-1-onto→wf1o 5122  ‘cfv 5123  2nd c2nd 6037   ≈ cen 6632  CCHOICEwacc 7082 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-iinf 4502 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-id 4215  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-2nd 6039  df-er 6429  df-en 6635  df-cc 7083 This theorem is referenced by:  cc2  7087
 Copyright terms: Public domain W3C validator