Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  ptcmplem3 Structured version   Visualization version   GIF version

Theorem ptcmplem3 22079
 Description: Lemma for ptcmp 22083. (Contributed by Mario Carneiro, 26-Aug-2015.)
Hypotheses
Ref Expression
ptcmp.1 𝑆 = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
ptcmp.2 𝑋 = X𝑛𝐴 (𝐹𝑛)
ptcmp.3 (𝜑𝐴𝑉)
ptcmp.4 (𝜑𝐹:𝐴⟶Comp)
ptcmp.5 (𝜑𝑋 ∈ (UFL ∩ dom card))
ptcmplem2.5 (𝜑𝑈 ⊆ ran 𝑆)
ptcmplem2.6 (𝜑𝑋 = 𝑈)
ptcmplem2.7 (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
ptcmplem3.8 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
Assertion
Ref Expression
ptcmplem3 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
Distinct variable groups:   𝑓,𝑘,𝑛,𝑢,𝑤,𝑧,𝐴   𝑓,𝐾,𝑢   𝑆,𝑘,𝑛,𝑢,𝑧   𝜑,𝑓,𝑘,𝑛,𝑢   𝑈,𝑘,𝑢,𝑧   𝑘,𝑉,𝑛,𝑢,𝑤,𝑧   𝑓,𝐹,𝑘,𝑛,𝑢,𝑤,𝑧   𝑓,𝑋,𝑘,𝑛,𝑢,𝑤,𝑧
Allowed substitution hints:   𝜑(𝑧,𝑤)   𝑆(𝑤,𝑓)   𝑈(𝑤,𝑓,𝑛)   𝐾(𝑧,𝑤,𝑘,𝑛)   𝑉(𝑓)

Proof of Theorem ptcmplem3
Dummy variables 𝑔 𝑚 𝑡 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ptcmp.3 . . . 4 (𝜑𝐴𝑉)
2 rabexg 4963 . . . 4 (𝐴𝑉 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} ∈ V)
31, 2syl 17 . . 3 (𝜑 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} ∈ V)
4 ptcmp.1 . . . . 5 𝑆 = (𝑘𝐴, 𝑢 ∈ (𝐹𝑘) ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢))
5 ptcmp.2 . . . . 5 𝑋 = X𝑛𝐴 (𝐹𝑛)
6 ptcmp.4 . . . . 5 (𝜑𝐹:𝐴⟶Comp)
7 ptcmp.5 . . . . 5 (𝜑𝑋 ∈ (UFL ∩ dom card))
8 ptcmplem2.5 . . . . 5 (𝜑𝑈 ⊆ ran 𝑆)
9 ptcmplem2.6 . . . . 5 (𝜑𝑋 = 𝑈)
10 ptcmplem2.7 . . . . 5 (𝜑 → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
114, 5, 1, 6, 7, 8, 9, 10ptcmplem2 22078 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘) ∈ dom card)
12 eldifi 3875 . . . . . . . 8 (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) → 𝑦 (𝐹𝑘))
13123ad2ant3 1130 . . . . . . 7 ((𝜑𝑦 ∈ V ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
1413rabssdv 3823 . . . . . 6 (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
1514ralrimivw 3105 . . . . 5 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
16 ss2iun 4688 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘))
1715, 16syl 17 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘))
18 ssnum 9072 . . . 4 (( 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘)) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
1911, 17, 18syl2anc 696 . . 3 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
20 elrabi 3499 . . . . 5 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} → 𝑘𝐴)
2110adantr 472 . . . . . . . 8 ((𝜑𝑘𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
22 ssdif0 4085 . . . . . . . . 9 ( (𝐹𝑘) ⊆ 𝐾 ↔ ( (𝐹𝑘) ∖ 𝐾) = ∅)
236ffvelrnda 6523 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Comp)
2423adantr 472 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ∈ Comp)
25 ptcmplem3.8 . . . . . . . . . . . . . 14 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
26 ssrab2 3828 . . . . . . . . . . . . . 14 {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈} ⊆ (𝐹𝑘)
2725, 26eqsstri 3776 . . . . . . . . . . . . 13 𝐾 ⊆ (𝐹𝑘)
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 ⊆ (𝐹𝑘))
29 simpr 479 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ⊆ 𝐾)
30 uniss 4610 . . . . . . . . . . . . . 14 (𝐾 ⊆ (𝐹𝑘) → 𝐾 (𝐹𝑘))
3127, 30mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 (𝐹𝑘))
3229, 31eqssd 3761 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) = 𝐾)
33 eqid 2760 . . . . . . . . . . . . 13 (𝐹𝑘) = (𝐹𝑘)
3433cmpcov 21414 . . . . . . . . . . . 12 (((𝐹𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹𝑘) ∧ (𝐹𝑘) = 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
3524, 28, 32, 34syl3anc 1477 . . . . . . . . . . 11 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
36 elfpw 8435 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡𝐾𝑡 ∈ Fin))
3736simplbi 478 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡𝐾)
3837ad2antrl 766 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡𝐾)
3938sselda 3744 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → 𝑥𝐾)
40 imaeq2 5620 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4140eleq1d 2824 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → (((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈 ↔ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4241, 25elrab2 3507 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↔ (𝑥 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4342simprbi 483 . . . . . . . . . . . . . . . 16 (𝑥𝐾 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4439, 43syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
45 eqid 2760 . . . . . . . . . . . . . . 15 (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4644, 45fmptd 6549 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)):𝑡𝑈)
47 frn 6214 . . . . . . . . . . . . . 14 ((𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)):𝑡𝑈 → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
4846, 47syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
4936simprbi 483 . . . . . . . . . . . . . . 15 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
5049ad2antrl 766 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡 ∈ Fin)
5145rnmpt 5526 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
52 abrexfi 8433 . . . . . . . . . . . . . . 15 (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)} ∈ Fin)
5351, 52syl5eqel 2843 . . . . . . . . . . . . . 14 (𝑡 ∈ Fin → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
5450, 53syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
55 elfpw 8435 . . . . . . . . . . . . 13 (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin))
5648, 54, 55sylanbrc 701 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
57 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
58 fveq2 6353 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
5958unieqd 4598 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
6057, 59eleq12d 2833 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
61 simpr 479 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓𝑋)
6261, 5syl6eleq 2849 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
63 vex 3343 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
6463elixp 8083 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
6564simprbi 483 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
6662, 65syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
67 simp-4r 827 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑘𝐴)
6860, 66, 67rspcdva 3455 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ (𝐹𝑘))
69 simplrr 820 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝐹𝑘) = 𝑡)
7068, 69eleqtrd 2841 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ 𝑡)
71 eluni2 4592 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑘) ∈ 𝑡 ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
7270, 71sylib 208 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
73 fveq1 6352 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
7473eleq1d 2824 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑥 ↔ (𝑓𝑘) ∈ 𝑥))
75 eqid 2760 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
7675mptpreima 5789 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑥}
7774, 76elrab2 3507 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑥))
7877baib 982 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑋 → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7978ad2antlr 765 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) ∧ 𝑥𝑡) → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
8079rexbidva 3187 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥))
8172, 80mpbird 247 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
82 eliun 4676 . . . . . . . . . . . . . . . . 17 (𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8381, 82sylibr 224 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8483ex 449 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑓𝑋𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8584ssrdv 3750 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8644ralrimiva 3104 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
87 dfiun2g 4704 . . . . . . . . . . . . . . . 16 (∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8886, 87syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8951unieqi 4597 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
9088, 89syl6eqr 2812 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9185, 90sseqtrd 3782 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9248unissd 4614 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
939ad3antrrr 768 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = 𝑈)
9492, 93sseqtr4d 3783 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑋)
9591, 94eqssd 3761 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
96 unieq 4596 . . . . . . . . . . . . . 14 (𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) → 𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9796eqeq2d 2770 . . . . . . . . . . . . 13 (𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) → (𝑋 = 𝑧𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))))
9897rspcev 3449 . . . . . . . . . . . 12 ((ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9956, 95, 98syl2anc 696 . . . . . . . . . . 11 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
10035, 99rexlimddv 3173 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
101100ex 449 . . . . . . . . 9 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ⊆ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10222, 101syl5bir 233 . . . . . . . 8 ((𝜑𝑘𝐴) → (( (𝐹𝑘) ∖ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10321, 102mtod 189 . . . . . . 7 ((𝜑𝑘𝐴) → ¬ ( (𝐹𝑘) ∖ 𝐾) = ∅)
104 neq0 4073 . . . . . . 7 (¬ ( (𝐹𝑘) ∖ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
105103, 104sylib 208 . . . . . 6 ((𝜑𝑘𝐴) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
106 rexv 3360 . . . . . 6 (∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
107105, 106sylibr 224 . . . . 5 ((𝜑𝑘𝐴) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
10820, 107sylan2 492 . . . 4 ((𝜑𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
109108ralrimiva 3104 . . 3 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
110 eleq1 2827 . . . 4 (𝑦 = (𝑔𝑘) → (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
111110ac6num 9513 . . 3 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1123, 19, 109, 111syl3anc 1477 . 2 (𝜑 → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1131adantr 472 . . . 4 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝐴𝑉)
114 mptexg 6649 . . . 4 (𝐴𝑉 → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V)
115113, 114syl 17 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V)
116 fvex 6363 . . . . . . . 8 (𝐹𝑚) ∈ V
117116uniex 7119 . . . . . . 7 (𝐹𝑚) ∈ V
118117uniex 7119 . . . . . 6 (𝐹𝑚) ∈ V
119 fvex 6363 . . . . . 6 (𝑔𝑚) ∈ V
120118, 119ifex 4300 . . . . 5 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V
121120rgenw 3062 . . . 4 𝑚𝐴 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V
122 eqid 2760 . . . . 5 (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))
123122fnmpt 6181 . . . 4 (∀𝑚𝐴 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
124121, 123mp1i 13 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
12559breq1d 4814 . . . . . . 7 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1𝑜 (𝐹𝑘) ≈ 1𝑜))
126125notbid 307 . . . . . 6 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1𝑜 ↔ ¬ (𝐹𝑘) ≈ 1𝑜))
127126ralrab 3509 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
128 iftrue 4236 . . . . . . . . . . 11 ( (𝐹𝑘) ≈ 1𝑜 → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
129128ad2antll 767 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
130105adantrr 755 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
13112adantl 473 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
132 simplrr 820 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ≈ 1𝑜)
133 en1b 8191 . . . . . . . . . . . . . . . 16 ( (𝐹𝑘) ≈ 1𝑜 (𝐹𝑘) = { (𝐹𝑘)})
134132, 133sylib 208 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) = { (𝐹𝑘)})
135131, 134eleqtrd 2841 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ { (𝐹𝑘)})
136 elsni 4338 . . . . . . . . . . . . . 14 (𝑦 ∈ { (𝐹𝑘)} → 𝑦 = (𝐹𝑘))
137135, 136syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 = (𝐹𝑘))
138 simpr 479 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
139137, 138eqeltrrd 2840 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
140130, 139exlimddv 2012 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
141140adantlr 753 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
142129, 141eqeltrd 2839 . . . . . . . . 9 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
143142a1d 25 . . . . . . . 8 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
144143expr 644 . . . . . . 7 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘𝐴) → ( (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
145 pm2.27 42 . . . . . . . 8 (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
146 iffalse 4239 . . . . . . . . 9 (𝐹𝑘) ≈ 1𝑜 → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝑔𝑘))
147146eleq1d 2824 . . . . . . . 8 (𝐹𝑘) ≈ 1𝑜 → (if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
148145, 147sylibrd 249 . . . . . . 7 (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
149144, 148pm2.61d1 171 . . . . . 6 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘𝐴) → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
150149ralimdva 3100 . . . . 5 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) → (∀𝑘𝐴 (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
151127, 150syl5bi 232 . . . 4 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) → (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
152151impr 650 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
153 fneq1 6140 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴))
154 fveq1 6352 . . . . . . . . 9 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (𝑓𝑘) = ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))‘𝑘))
155 fveq2 6353 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
156155unieqd 4598 . . . . . . . . . . . 12 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
157156breq1d 4814 . . . . . . . . . . 11 (𝑚 = 𝑘 → ( (𝐹𝑚) ≈ 1𝑜 (𝐹𝑘) ≈ 1𝑜))
158156unieqd 4598 . . . . . . . . . . 11 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
159 fveq2 6353 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑔𝑚) = (𝑔𝑘))
160157, 158, 159ifbieq12d 4257 . . . . . . . . . 10 (𝑚 = 𝑘 → if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
161 fvex 6363 . . . . . . . . . . . . 13 (𝐹𝑘) ∈ V
162161uniex 7119 . . . . . . . . . . . 12 (𝐹𝑘) ∈ V
163162uniex 7119 . . . . . . . . . . 11 (𝐹𝑘) ∈ V
164 fvex 6363 . . . . . . . . . . 11 (𝑔𝑘) ∈ V
165163, 164ifex 4300 . . . . . . . . . 10 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ V
166160, 122, 165fvmpt 6445 . . . . . . . . 9 (𝑘𝐴 → ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))‘𝑘) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
167154, 166sylan9eq 2814 . . . . . . . 8 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → (𝑓𝑘) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
168167eleq1d 2824 . . . . . . 7 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
169168ralbidva 3123 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
170153, 169anbi12d 749 . . . . 5 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) ↔ ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
171170spcegv 3434 . . . 4 ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V → (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))))
1721713impib 1109 . . 3 (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V ∧ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
173115, 124, 152, 172syl3anc 1477 . 2 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
174112, 173exlimddv 2012 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632  ∃wex 1853   ∈ wcel 2139  {cab 2746  ∀wral 3050  ∃wrex 3051  {crab 3054  Vcvv 3340   ∖ cdif 3712   ∩ cin 3714   ⊆ wss 3715  ∅c0 4058  ifcif 4230  𝒫 cpw 4302  {csn 4321  ∪ cuni 4588  ∪ ciun 4672   class class class wbr 4804   ↦ cmpt 4881  ◡ccnv 5265  dom cdm 5266  ran crn 5267   “ cima 5269   Fn wfn 6044  ⟶wf 6045  ‘cfv 6049   ↦ cmpt2 6816  1𝑜c1o 7723  Xcixp 8076   ≈ cen 8120  Fincfn 8123  cardccrd 8971  Compccmp 21411  UFLcufl 21925 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6775  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-om 7232  df-1st 7334  df-2nd 7335  df-wrecs 7577  df-recs 7638  df-rdg 7676  df-1o 7730  df-oadd 7734  df-omul 7735  df-er 7913  df-map 8027  df-ixp 8077  df-en 8124  df-dom 8125  df-fin 8127  df-wdom 8631  df-card 8975  df-acn 8978  df-cmp 21412 This theorem is referenced by:  ptcmplem4  22080
 Copyright terms: Public domain W3C validator