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

Theorem cc3 7088
 Description: Countable choice using a sequence F(n) . (Contributed by Mario Carneiro, 8-Feb-2013.) (Revised by Jim Kingdon, 29-Apr-2024.)
Hypotheses
Ref Expression
cc3.cc (𝜑CCHOICE)
cc3.f (𝜑 → ∀𝑛𝑁 𝐹 ∈ V)
cc3.m (𝜑 → ∀𝑛𝑁𝑤 𝑤𝐹)
cc3.n (𝜑𝑁 ≈ ω)
Assertion
Ref Expression
cc3 (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
Distinct variable groups:   𝑓,𝐹   𝑤,𝐹   𝑓,𝑁,𝑛   𝑤,𝑁,𝑛   𝜑,𝑛,𝑤
Allowed substitution hints:   𝜑(𝑓)   𝐹(𝑛)

Proof of Theorem cc3
Dummy variables 𝑔 𝑘 𝑚 𝑝 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cc3.n . . 3 (𝜑𝑁 ≈ ω)
2 relen 6638 . . . 4 Rel ≈
32brrelex1i 4582 . . 3 (𝑁 ≈ ω → 𝑁 ∈ V)
4 mptexg 5645 . . 3 (𝑁 ∈ V → (𝑛𝑁𝐹) ∈ V)
51, 3, 43syl 17 . 2 (𝜑 → (𝑛𝑁𝐹) ∈ V)
6 bren 6641 . . . . . . 7 (𝑁 ≈ ω ↔ ∃ :𝑁1-1-onto→ω)
71, 6sylib 121 . . . . . 6 (𝜑 → ∃ :𝑁1-1-onto→ω)
87adantr 274 . . . . 5 ((𝜑𝑘 = (𝑛𝑁𝐹)) → ∃ :𝑁1-1-onto→ω)
9 cc3.cc . . . . . . . 8 (𝜑CCHOICE)
109ad2antrr 479 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → CCHOICE)
11 cc3.f . . . . . . . . . . . 12 (𝜑 → ∀𝑛𝑁 𝐹 ∈ V)
12 eqid 2139 . . . . . . . . . . . . 13 (𝑛𝑁𝐹) = (𝑛𝑁𝐹)
1312mptfng 5248 . . . . . . . . . . . 12 (∀𝑛𝑁 𝐹 ∈ V ↔ (𝑛𝑁𝐹) Fn 𝑁)
1411, 13sylib 121 . . . . . . . . . . 11 (𝜑 → (𝑛𝑁𝐹) Fn 𝑁)
1514adantr 274 . . . . . . . . . 10 ((𝜑𝑘 = (𝑛𝑁𝐹)) → (𝑛𝑁𝐹) Fn 𝑁)
16 simpr 109 . . . . . . . . . . 11 ((𝜑𝑘 = (𝑛𝑁𝐹)) → 𝑘 = (𝑛𝑁𝐹))
1716fneq1d 5213 . . . . . . . . . 10 ((𝜑𝑘 = (𝑛𝑁𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛𝑁𝐹) Fn 𝑁))
1815, 17mpbird 166 . . . . . . . . 9 ((𝜑𝑘 = (𝑛𝑁𝐹)) → 𝑘 Fn 𝑁)
1918adantr 274 . . . . . . . 8 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → 𝑘 Fn 𝑁)
20 f1ocnv 5380 . . . . . . . . . 10 (:𝑁1-1-onto→ω → :ω–1-1-onto𝑁)
2120adantl 275 . . . . . . . . 9 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :ω–1-1-onto𝑁)
22 f1of 5367 . . . . . . . . 9 (:ω–1-1-onto𝑁:ω⟶𝑁)
2321, 22syl 14 . . . . . . . 8 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :ω⟶𝑁)
24 fnfco 5297 . . . . . . . 8 ((𝑘 Fn 𝑁:ω⟶𝑁) → (𝑘) Fn ω)
2519, 23, 24syl2anc 408 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → (𝑘) Fn ω)
2623ffvelrnda 5555 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑝) ∈ 𝑁)
27 cc3.m . . . . . . . . . . 11 (𝜑 → ∀𝑛𝑁𝑤 𝑤𝐹)
2827ad3antrrr 483 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛𝑁𝑤 𝑤𝐹)
29 nfcsb1v 3035 . . . . . . . . . . . . 13 𝑛(𝑝) / 𝑛𝐹
3029nfcri 2275 . . . . . . . . . . . 12 𝑛 𝑤(𝑝) / 𝑛𝐹
3130nfex 1616 . . . . . . . . . . 11 𝑛𝑤 𝑤(𝑝) / 𝑛𝐹
32 csbeq1a 3012 . . . . . . . . . . . . 13 (𝑛 = (𝑝) → 𝐹 = (𝑝) / 𝑛𝐹)
3332eleq2d 2209 . . . . . . . . . . . 12 (𝑛 = (𝑝) → (𝑤𝐹𝑤(𝑝) / 𝑛𝐹))
3433exbidv 1797 . . . . . . . . . . 11 (𝑛 = (𝑝) → (∃𝑤 𝑤𝐹 ↔ ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
3531, 34rspc 2783 . . . . . . . . . 10 ((𝑝) ∈ 𝑁 → (∀𝑛𝑁𝑤 𝑤𝐹 → ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
3626, 28, 35sylc 62 . . . . . . . . 9 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤(𝑝) / 𝑛𝐹)
37 fvco3 5492 . . . . . . . . . . . . 13 ((:ω⟶𝑁𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑘‘(𝑝)))
3823, 37sylan 281 . . . . . . . . . . . 12 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑘‘(𝑝)))
39 simpllr 523 . . . . . . . . . . . . . 14 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛𝑁𝐹))
4039fveq1d 5423 . . . . . . . . . . . . 13 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(𝑝)) = ((𝑛𝑁𝐹)‘(𝑝)))
4111ad3antrrr 483 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛𝑁 𝐹 ∈ V)
4229nfel1 2292 . . . . . . . . . . . . . . . 16 𝑛(𝑝) / 𝑛𝐹 ∈ V
4332eleq1d 2208 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑝) → (𝐹 ∈ V ↔ (𝑝) / 𝑛𝐹 ∈ V))
4442, 43rspc 2783 . . . . . . . . . . . . . . 15 ((𝑝) ∈ 𝑁 → (∀𝑛𝑁 𝐹 ∈ V → (𝑝) / 𝑛𝐹 ∈ V))
4526, 41, 44sylc 62 . . . . . . . . . . . . . 14 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑝) / 𝑛𝐹 ∈ V)
4612fvmpts 5499 . . . . . . . . . . . . . 14 (((𝑝) ∈ 𝑁(𝑝) / 𝑛𝐹 ∈ V) → ((𝑛𝑁𝐹)‘(𝑝)) = (𝑝) / 𝑛𝐹)
4726, 45, 46syl2anc 408 . . . . . . . . . . . . 13 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛𝑁𝐹)‘(𝑝)) = (𝑝) / 𝑛𝐹)
4840, 47eqtrd 2172 . . . . . . . . . . . 12 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(𝑝)) = (𝑝) / 𝑛𝐹)
4938, 48eqtrd 2172 . . . . . . . . . . 11 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑝) / 𝑛𝐹)
5049eleq2d 2209 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘)‘𝑝) ↔ 𝑤(𝑝) / 𝑛𝐹))
5150exbidv 1797 . . . . . . . . 9 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘)‘𝑝) ↔ ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
5236, 51mpbird 166 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘)‘𝑝))
5352ralrimiva 2505 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘)‘𝑝))
5410, 25, 53cc2 7087 . . . . . 6 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚)))
55 simprl 520 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → 𝑔 Fn ω)
56 f1of 5367 . . . . . . . . . 10 (:𝑁1-1-onto→ω → :𝑁⟶ω)
5756adantl 275 . . . . . . . . 9 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :𝑁⟶ω)
5857adantr 274 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → :𝑁⟶ω)
59 fnfco 5297 . . . . . . . 8 ((𝑔 Fn ω ∧ :𝑁⟶ω) → (𝑔) Fn 𝑁)
6055, 58, 59syl2anc 408 . . . . . . 7 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → (𝑔) Fn 𝑁)
61 nfv 1508 . . . . . . . . . . 11 𝑛𝜑
62 nfmpt1 4021 . . . . . . . . . . . 12 𝑛(𝑛𝑁𝐹)
6362nfeq2 2293 . . . . . . . . . . 11 𝑛 𝑘 = (𝑛𝑁𝐹)
6461, 63nfan 1544 . . . . . . . . . 10 𝑛(𝜑𝑘 = (𝑛𝑁𝐹))
65 nfv 1508 . . . . . . . . . 10 𝑛 :𝑁1-1-onto→ω
6664, 65nfan 1544 . . . . . . . . 9 𝑛((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω)
67 nfv 1508 . . . . . . . . 9 𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))
6866, 67nfan 1544 . . . . . . . 8 𝑛(((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚)))
69 fvco3 5492 . . . . . . . . . . . . . 14 ((:𝑁⟶ω ∧ 𝑛𝑁) → ((𝑔)‘𝑛) = (𝑔‘(𝑛)))
7058, 69sylan 281 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) = (𝑔‘(𝑛)))
71 fveq2 5421 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛) → (𝑔𝑚) = (𝑔‘(𝑛)))
72 fveq2 5421 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛) → ((𝑘)‘𝑚) = ((𝑘)‘(𝑛)))
7371, 72eleq12d 2210 . . . . . . . . . . . . . 14 (𝑚 = (𝑛) → ((𝑔𝑚) ∈ ((𝑘)‘𝑚) ↔ (𝑔‘(𝑛)) ∈ ((𝑘)‘(𝑛))))
74 simplrr 525 . . . . . . . . . . . . . 14 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))
7558ffvelrnda 5555 . . . . . . . . . . . . . 14 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑛) ∈ ω)
7673, 74, 75rspcdva 2794 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑔‘(𝑛)) ∈ ((𝑘)‘(𝑛)))
7770, 76eqeltrd 2216 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ ((𝑘)‘(𝑛)))
7823ad2antrr 479 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → :ω⟶𝑁)
79 fvco3 5492 . . . . . . . . . . . . 13 ((:ω⟶𝑁 ∧ (𝑛) ∈ ω) → ((𝑘)‘(𝑛)) = (𝑘‘(‘(𝑛))))
8078, 75, 79syl2anc 408 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑘)‘(𝑛)) = (𝑘‘(‘(𝑛))))
8177, 80eleqtrd 2218 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ (𝑘‘(‘(𝑛))))
82 simpllr 523 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → :𝑁1-1-onto→ω)
83 simpr 109 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝑛𝑁)
84 f1ocnvfv1 5678 . . . . . . . . . . . . 13 ((:𝑁1-1-onto→ω ∧ 𝑛𝑁) → (‘(𝑛)) = 𝑛)
8582, 83, 84syl2anc 408 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (‘(𝑛)) = 𝑛)
8685fveq2d 5425 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘‘(‘(𝑛))) = (𝑘𝑛))
8781, 86eleqtrd 2218 . . . . . . . . . 10 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ (𝑘𝑛))
8816ad3antrrr 483 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝑘 = (𝑛𝑁𝐹))
8988fveq1d 5423 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘𝑛) = ((𝑛𝑁𝐹)‘𝑛))
9011r19.21bi 2520 . . . . . . . . . . . . 13 ((𝜑𝑛𝑁) → 𝐹 ∈ V)
9190ad5ant15 512 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝐹 ∈ V)
9212fvmpt2 5504 . . . . . . . . . . . 12 ((𝑛𝑁𝐹 ∈ V) → ((𝑛𝑁𝐹)‘𝑛) = 𝐹)
9383, 91, 92syl2anc 408 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑛𝑁𝐹)‘𝑛) = 𝐹)
9489, 93eqtrd 2172 . . . . . . . . . 10 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘𝑛) = 𝐹)
9587, 94eleqtrd 2218 . . . . . . . . 9 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ 𝐹)
9695ex 114 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → (𝑛𝑁 → ((𝑔)‘𝑛) ∈ 𝐹))
9768, 96ralrimi 2503 . . . . . . 7 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹)
98 vex 2689 . . . . . . . . 9 𝑔 ∈ V
99 vex 2689 . . . . . . . . 9 ∈ V
10098, 99coex 5084 . . . . . . . 8 (𝑔) ∈ V
101 fneq1 5211 . . . . . . . . 9 (𝑓 = (𝑔) → (𝑓 Fn 𝑁 ↔ (𝑔) Fn 𝑁))
102 fveq1 5420 . . . . . . . . . . 11 (𝑓 = (𝑔) → (𝑓𝑛) = ((𝑔)‘𝑛))
103102eleq1d 2208 . . . . . . . . . 10 (𝑓 = (𝑔) → ((𝑓𝑛) ∈ 𝐹 ↔ ((𝑔)‘𝑛) ∈ 𝐹))
104103ralbidv 2437 . . . . . . . . 9 (𝑓 = (𝑔) → (∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹 ↔ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹))
105101, 104anbi12d 464 . . . . . . . 8 (𝑓 = (𝑔) → ((𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹) ↔ ((𝑔) Fn 𝑁 ∧ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹)))
106100, 105spcev 2780 . . . . . . 7 (((𝑔) Fn 𝑁 ∧ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
10760, 97, 106syl2anc 408 . . . . . 6 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
10854, 107exlimddv 1870 . . . . 5 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
1098, 108exlimddv 1870 . . . 4 ((𝜑𝑘 = (𝑛𝑁𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
110109expcom 115 . . 3 (𝑘 = (𝑛𝑁𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹)))
111110vtocleg 2757 . 2 ((𝑛𝑁𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹)))
1125, 111mpcom 36 1 (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  ∃wex 1468   ∈ wcel 1480  ∀wral 2416  Vcvv 2686  ⦋csb 3003   class class class wbr 3929   ↦ cmpt 3989  ωcom 4504  ◡ccnv 4538   ∘ ccom 4543   Fn wfn 5118  ⟶wf 5119  –1-1-onto→wf1o 5122  ‘cfv 5123   ≈ 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:  cc4f  7089  cc4n  7091
 Copyright terms: Public domain W3C validator