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

Theorem cc3 7217
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 6718 . . . 4 Rel ≈
32brrelex1i 4652 . . 3 (𝑁 ≈ ω → 𝑁 ∈ V)
4 mptexg 5718 . . 3 (𝑁 ∈ V → (𝑛𝑁𝐹) ∈ V)
51, 3, 43syl 17 . 2 (𝜑 → (𝑛𝑁𝐹) ∈ V)
6 bren 6721 . . . . . . 7 (𝑁 ≈ ω ↔ ∃ :𝑁1-1-onto→ω)
71, 6sylib 121 . . . . . 6 (𝜑 → ∃ :𝑁1-1-onto→ω)
87adantr 274 . . . . 5 ((𝜑𝑘 = (𝑛𝑁𝐹)) → ∃ :𝑁1-1-onto→ω)
9 cc3.cc . . . . . . . 8 (𝜑CCHOICE)
109ad2antrr 485 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → CCHOICE)
11 cc3.f . . . . . . . . . . . 12 (𝜑 → ∀𝑛𝑁 𝐹 ∈ V)
12 eqid 2170 . . . . . . . . . . . . 13 (𝑛𝑁𝐹) = (𝑛𝑁𝐹)
1312mptfng 5321 . . . . . . . . . . . 12 (∀𝑛𝑁 𝐹 ∈ V ↔ (𝑛𝑁𝐹) Fn 𝑁)
1411, 13sylib 121 . . . . . . . . . . 11 (𝜑 → (𝑛𝑁𝐹) Fn 𝑁)
1514adantr 274 . . . . . . . . . 10 ((𝜑𝑘 = (𝑛𝑁𝐹)) → (𝑛𝑁𝐹) Fn 𝑁)
16 simpr 109 . . . . . . . . . . 11 ((𝜑𝑘 = (𝑛𝑁𝐹)) → 𝑘 = (𝑛𝑁𝐹))
1716fneq1d 5286 . . . . . . . . . 10 ((𝜑𝑘 = (𝑛𝑁𝐹)) → (𝑘 Fn 𝑁 ↔ (𝑛𝑁𝐹) Fn 𝑁))
1815, 17mpbird 166 . . . . . . . . 9 ((𝜑𝑘 = (𝑛𝑁𝐹)) → 𝑘 Fn 𝑁)
1918adantr 274 . . . . . . . 8 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → 𝑘 Fn 𝑁)
20 f1ocnv 5453 . . . . . . . . . 10 (:𝑁1-1-onto→ω → :ω–1-1-onto𝑁)
2120adantl 275 . . . . . . . . 9 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :ω–1-1-onto𝑁)
22 f1of 5440 . . . . . . . . 9 (:ω–1-1-onto𝑁:ω⟶𝑁)
2321, 22syl 14 . . . . . . . 8 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :ω⟶𝑁)
24 fnfco 5370 . . . . . . . 8 ((𝑘 Fn 𝑁:ω⟶𝑁) → (𝑘) Fn ω)
2519, 23, 24syl2anc 409 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → (𝑘) Fn ω)
2623ffvelrnda 5628 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑝) ∈ 𝑁)
27 cc3.m . . . . . . . . . . 11 (𝜑 → ∀𝑛𝑁𝑤 𝑤𝐹)
2827ad3antrrr 489 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛𝑁𝑤 𝑤𝐹)
29 nfcsb1v 3082 . . . . . . . . . . . . 13 𝑛(𝑝) / 𝑛𝐹
3029nfcri 2306 . . . . . . . . . . . 12 𝑛 𝑤(𝑝) / 𝑛𝐹
3130nfex 1630 . . . . . . . . . . 11 𝑛𝑤 𝑤(𝑝) / 𝑛𝐹
32 csbeq1a 3058 . . . . . . . . . . . . 13 (𝑛 = (𝑝) → 𝐹 = (𝑝) / 𝑛𝐹)
3332eleq2d 2240 . . . . . . . . . . . 12 (𝑛 = (𝑝) → (𝑤𝐹𝑤(𝑝) / 𝑛𝐹))
3433exbidv 1818 . . . . . . . . . . 11 (𝑛 = (𝑝) → (∃𝑤 𝑤𝐹 ↔ ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
3531, 34rspc 2828 . . . . . . . . . 10 ((𝑝) ∈ 𝑁 → (∀𝑛𝑁𝑤 𝑤𝐹 → ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
3626, 28, 35sylc 62 . . . . . . . . 9 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤(𝑝) / 𝑛𝐹)
37 fvco3 5565 . . . . . . . . . . . . 13 ((:ω⟶𝑁𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑘‘(𝑝)))
3823, 37sylan 281 . . . . . . . . . . . 12 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑘‘(𝑝)))
39 simpllr 529 . . . . . . . . . . . . . 14 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → 𝑘 = (𝑛𝑁𝐹))
4039fveq1d 5496 . . . . . . . . . . . . 13 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(𝑝)) = ((𝑛𝑁𝐹)‘(𝑝)))
4111ad3antrrr 489 . . . . . . . . . . . . . . 15 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∀𝑛𝑁 𝐹 ∈ V)
4229nfel1 2323 . . . . . . . . . . . . . . . 16 𝑛(𝑝) / 𝑛𝐹 ∈ V
4332eleq1d 2239 . . . . . . . . . . . . . . . 16 (𝑛 = (𝑝) → (𝐹 ∈ V ↔ (𝑝) / 𝑛𝐹 ∈ V))
4442, 43rspc 2828 . . . . . . . . . . . . . . 15 ((𝑝) ∈ 𝑁 → (∀𝑛𝑁 𝐹 ∈ V → (𝑝) / 𝑛𝐹 ∈ V))
4526, 41, 44sylc 62 . . . . . . . . . . . . . 14 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑝) / 𝑛𝐹 ∈ V)
4612fvmpts 5572 . . . . . . . . . . . . . 14 (((𝑝) ∈ 𝑁(𝑝) / 𝑛𝐹 ∈ V) → ((𝑛𝑁𝐹)‘(𝑝)) = (𝑝) / 𝑛𝐹)
4726, 45, 46syl2anc 409 . . . . . . . . . . . . 13 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑛𝑁𝐹)‘(𝑝)) = (𝑝) / 𝑛𝐹)
4840, 47eqtrd 2203 . . . . . . . . . . . 12 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑘‘(𝑝)) = (𝑝) / 𝑛𝐹)
4938, 48eqtrd 2203 . . . . . . . . . . 11 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ((𝑘)‘𝑝) = (𝑝) / 𝑛𝐹)
5049eleq2d 2240 . . . . . . . . . 10 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (𝑤 ∈ ((𝑘)‘𝑝) ↔ 𝑤(𝑝) / 𝑛𝐹))
5150exbidv 1818 . . . . . . . . 9 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → (∃𝑤 𝑤 ∈ ((𝑘)‘𝑝) ↔ ∃𝑤 𝑤(𝑝) / 𝑛𝐹))
5236, 51mpbird 166 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ 𝑝 ∈ ω) → ∃𝑤 𝑤 ∈ ((𝑘)‘𝑝))
5352ralrimiva 2543 . . . . . . 7 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∀𝑝 ∈ ω ∃𝑤 𝑤 ∈ ((𝑘)‘𝑝))
5410, 25, 53cc2 7216 . . . . . 6 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∃𝑔(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚)))
55 simprl 526 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → 𝑔 Fn ω)
56 f1of 5440 . . . . . . . . . 10 (:𝑁1-1-onto→ω → :𝑁⟶ω)
5756adantl 275 . . . . . . . . 9 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → :𝑁⟶ω)
5857adantr 274 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → :𝑁⟶ω)
59 fnfco 5370 . . . . . . . 8 ((𝑔 Fn ω ∧ :𝑁⟶ω) → (𝑔) Fn 𝑁)
6055, 58, 59syl2anc 409 . . . . . . 7 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → (𝑔) Fn 𝑁)
61 nfv 1521 . . . . . . . . . . 11 𝑛𝜑
62 nfmpt1 4080 . . . . . . . . . . . 12 𝑛(𝑛𝑁𝐹)
6362nfeq2 2324 . . . . . . . . . . 11 𝑛 𝑘 = (𝑛𝑁𝐹)
6461, 63nfan 1558 . . . . . . . . . 10 𝑛(𝜑𝑘 = (𝑛𝑁𝐹))
65 nfv 1521 . . . . . . . . . 10 𝑛 :𝑁1-1-onto→ω
6664, 65nfan 1558 . . . . . . . . 9 𝑛((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω)
67 nfv 1521 . . . . . . . . 9 𝑛(𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))
6866, 67nfan 1558 . . . . . . . 8 𝑛(((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚)))
69 fvco3 5565 . . . . . . . . . . . . . 14 ((:𝑁⟶ω ∧ 𝑛𝑁) → ((𝑔)‘𝑛) = (𝑔‘(𝑛)))
7058, 69sylan 281 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) = (𝑔‘(𝑛)))
71 fveq2 5494 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛) → (𝑔𝑚) = (𝑔‘(𝑛)))
72 fveq2 5494 . . . . . . . . . . . . . . 15 (𝑚 = (𝑛) → ((𝑘)‘𝑚) = ((𝑘)‘(𝑛)))
7371, 72eleq12d 2241 . . . . . . . . . . . . . 14 (𝑚 = (𝑛) → ((𝑔𝑚) ∈ ((𝑘)‘𝑚) ↔ (𝑔‘(𝑛)) ∈ ((𝑘)‘(𝑛))))
74 simplrr 531 . . . . . . . . . . . . . 14 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))
7558ffvelrnda 5628 . . . . . . . . . . . . . 14 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑛) ∈ ω)
7673, 74, 75rspcdva 2839 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑔‘(𝑛)) ∈ ((𝑘)‘(𝑛)))
7770, 76eqeltrd 2247 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ ((𝑘)‘(𝑛)))
7823ad2antrr 485 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → :ω⟶𝑁)
79 fvco3 5565 . . . . . . . . . . . . 13 ((:ω⟶𝑁 ∧ (𝑛) ∈ ω) → ((𝑘)‘(𝑛)) = (𝑘‘(‘(𝑛))))
8078, 75, 79syl2anc 409 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑘)‘(𝑛)) = (𝑘‘(‘(𝑛))))
8177, 80eleqtrd 2249 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ (𝑘‘(‘(𝑛))))
82 simpllr 529 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → :𝑁1-1-onto→ω)
83 simpr 109 . . . . . . . . . . . . 13 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝑛𝑁)
84 f1ocnvfv1 5753 . . . . . . . . . . . . 13 ((:𝑁1-1-onto→ω ∧ 𝑛𝑁) → (‘(𝑛)) = 𝑛)
8582, 83, 84syl2anc 409 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (‘(𝑛)) = 𝑛)
8685fveq2d 5498 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘‘(‘(𝑛))) = (𝑘𝑛))
8781, 86eleqtrd 2249 . . . . . . . . . 10 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ (𝑘𝑛))
8816ad3antrrr 489 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝑘 = (𝑛𝑁𝐹))
8988fveq1d 5496 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘𝑛) = ((𝑛𝑁𝐹)‘𝑛))
9011r19.21bi 2558 . . . . . . . . . . . . 13 ((𝜑𝑛𝑁) → 𝐹 ∈ V)
9190ad5ant15 518 . . . . . . . . . . . 12 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → 𝐹 ∈ V)
9212fvmpt2 5577 . . . . . . . . . . . 12 ((𝑛𝑁𝐹 ∈ V) → ((𝑛𝑁𝐹)‘𝑛) = 𝐹)
9383, 91, 92syl2anc 409 . . . . . . . . . . 11 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑛𝑁𝐹)‘𝑛) = 𝐹)
9489, 93eqtrd 2203 . . . . . . . . . 10 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → (𝑘𝑛) = 𝐹)
9587, 94eleqtrd 2249 . . . . . . . . 9 (((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) ∧ 𝑛𝑁) → ((𝑔)‘𝑛) ∈ 𝐹)
9695ex 114 . . . . . . . 8 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → (𝑛𝑁 → ((𝑔)‘𝑛) ∈ 𝐹))
9768, 96ralrimi 2541 . . . . . . 7 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹)
98 vex 2733 . . . . . . . . 9 𝑔 ∈ V
99 vex 2733 . . . . . . . . 9 ∈ V
10098, 99coex 5154 . . . . . . . 8 (𝑔) ∈ V
101 fneq1 5284 . . . . . . . . 9 (𝑓 = (𝑔) → (𝑓 Fn 𝑁 ↔ (𝑔) Fn 𝑁))
102 fveq1 5493 . . . . . . . . . . 11 (𝑓 = (𝑔) → (𝑓𝑛) = ((𝑔)‘𝑛))
103102eleq1d 2239 . . . . . . . . . 10 (𝑓 = (𝑔) → ((𝑓𝑛) ∈ 𝐹 ↔ ((𝑔)‘𝑛) ∈ 𝐹))
104103ralbidv 2470 . . . . . . . . 9 (𝑓 = (𝑔) → (∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹 ↔ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹))
105101, 104anbi12d 470 . . . . . . . 8 (𝑓 = (𝑔) → ((𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹) ↔ ((𝑔) Fn 𝑁 ∧ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹)))
106100, 105spcev 2825 . . . . . . 7 (((𝑔) Fn 𝑁 ∧ ∀𝑛𝑁 ((𝑔)‘𝑛) ∈ 𝐹) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
10760, 97, 106syl2anc 409 . . . . . 6 ((((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) ∧ (𝑔 Fn ω ∧ ∀𝑚 ∈ ω (𝑔𝑚) ∈ ((𝑘)‘𝑚))) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
10854, 107exlimddv 1891 . . . . 5 (((𝜑𝑘 = (𝑛𝑁𝐹)) ∧ :𝑁1-1-onto→ω) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
1098, 108exlimddv 1891 . . . 4 ((𝜑𝑘 = (𝑛𝑁𝐹)) → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
110109expcom 115 . . 3 (𝑘 = (𝑛𝑁𝐹) → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹)))
111110vtocleg 2801 . 2 ((𝑛𝑁𝐹) ∈ V → (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹)))
1125, 111mpcom 36 1 (𝜑 → ∃𝑓(𝑓 Fn 𝑁 ∧ ∀𝑛𝑁 (𝑓𝑛) ∈ 𝐹))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1348  wex 1485  wcel 2141  wral 2448  Vcvv 2730  csb 3049   class class class wbr 3987  cmpt 4048  ωcom 4572  ccnv 4608  ccom 4613   Fn wfn 5191  wf 5192  1-1-ontowf1o 5195  cfv 5196  cen 6712  CCHOICEwacc 7211
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 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4102  ax-sep 4105  ax-pow 4158  ax-pr 4192  ax-un 4416  ax-iinf 4570
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-un 3125  df-in 3127  df-ss 3134  df-pw 3566  df-sn 3587  df-pr 3588  df-op 3590  df-uni 3795  df-int 3830  df-iun 3873  df-br 3988  df-opab 4049  df-mpt 4050  df-id 4276  df-iom 4573  df-xp 4615  df-rel 4616  df-cnv 4617  df-co 4618  df-dm 4619  df-rn 4620  df-res 4621  df-ima 4622  df-iota 5158  df-fun 5198  df-fn 5199  df-f 5200  df-f1 5201  df-fo 5202  df-f1o 5203  df-fv 5204  df-2nd 6117  df-er 6509  df-en 6715  df-cc 7212
This theorem is referenced by:  cc4f  7218  cc4n  7220
  Copyright terms: Public domain W3C validator