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

Theorem ptcmplem3 22075
Description: Lemma for ptcmp 22079. (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 5013 . . . 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 22074 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘) ∈ dom card)
12 eldifi 3938 . . . . . . . 8 (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) → 𝑦 (𝐹𝑘))
13123ad2ant3 1158 . . . . . . 7 ((𝜑𝑦 ∈ V ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
1413rabssdv 3886 . . . . . 6 (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
1514ralrimivw 3162 . . . . 5 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
16 ss2iun 4735 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘))
1715, 16syl 17 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘))
18 ssnum 9148 . . . 4 (( 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝐹𝑘)) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
1911, 17, 18syl2anc 575 . . 3 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
20 elrabi 3561 . . . . 5 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} → 𝑘𝐴)
2110adantr 468 . . . . . . . 8 ((𝜑𝑘𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
22 ssdif0 4150 . . . . . . . . 9 ( (𝐹𝑘) ⊆ 𝐾 ↔ ( (𝐹𝑘) ∖ 𝐾) = ∅)
236ffvelrnda 6584 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Comp)
2423adantr 468 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ∈ Comp)
25 ptcmplem3.8 . . . . . . . . . . . . . 14 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
26 ssrab2 3891 . . . . . . . . . . . . . 14 {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈} ⊆ (𝐹𝑘)
2725, 26eqsstri 3839 . . . . . . . . . . . . 13 𝐾 ⊆ (𝐹𝑘)
2827a1i 11 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 ⊆ (𝐹𝑘))
29 simpr 473 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ⊆ 𝐾)
30 uniss 4660 . . . . . . . . . . . . . 14 (𝐾 ⊆ (𝐹𝑘) → 𝐾 (𝐹𝑘))
3127, 30mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 (𝐹𝑘))
3229, 31eqssd 3822 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) = 𝐾)
33 eqid 2813 . . . . . . . . . . . . 13 (𝐹𝑘) = (𝐹𝑘)
3433cmpcov 21410 . . . . . . . . . . . 12 (((𝐹𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹𝑘) ∧ (𝐹𝑘) = 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
3524, 28, 32, 34syl3anc 1483 . . . . . . . . . . 11 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
36 elfpw 8510 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡𝐾𝑡 ∈ Fin))
3736simplbi 487 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡𝐾)
3837ad2antrl 710 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡𝐾)
3938sselda 3805 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → 𝑥𝐾)
40 imaeq2 5679 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4140eleq1d 2877 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → (((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈 ↔ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4241, 25elrab2 3569 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↔ (𝑥 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4342simprbi 486 . . . . . . . . . . . . . . . 16 (𝑥𝐾 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4439, 43syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4544fmpttd 6610 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)):𝑡𝑈)
4645frnd 6266 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
4736simprbi 486 . . . . . . . . . . . . . . 15 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
4847ad2antrl 710 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡 ∈ Fin)
49 eqid 2813 . . . . . . . . . . . . . . . 16 (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
5049rnmpt 5579 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
51 abrexfi 8508 . . . . . . . . . . . . . . 15 (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)} ∈ Fin)
5250, 51syl5eqel 2896 . . . . . . . . . . . . . 14 (𝑡 ∈ Fin → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
5348, 52syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
54 elfpw 8510 . . . . . . . . . . . . 13 (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin))
5546, 53, 54sylanbrc 574 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
56 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
57 fveq2 6411 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
5857unieqd 4647 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
5956, 58eleq12d 2886 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
60 simpr 473 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓𝑋)
6160, 5syl6eleq 2902 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
62 vex 3401 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
6362elixp 8155 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
6463simprbi 486 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
6561, 64syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
66 simp-4r 794 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑘𝐴)
6759, 65, 66rspcdva 3515 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ (𝐹𝑘))
68 simplrr 787 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝐹𝑘) = 𝑡)
6967, 68eleqtrd 2894 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ 𝑡)
70 eluni2 4641 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑘) ∈ 𝑡 ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
7169, 70sylib 209 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
72 fveq1 6410 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
7372eleq1d 2877 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑥 ↔ (𝑓𝑘) ∈ 𝑥))
74 eqid 2813 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
7574mptpreima 5849 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑥}
7673, 75elrab2 3569 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑥))
7776baib 527 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑋 → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7877ad2antlr 709 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) ∧ 𝑥𝑡) → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7978rexbidva 3244 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥))
8071, 79mpbird 248 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
81 eliun 4723 . . . . . . . . . . . . . . . . 17 (𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8280, 81sylibr 225 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8382ex 399 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑓𝑋𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8483ssrdv 3811 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8544ralrimiva 3161 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
86 dfiun2g 4751 . . . . . . . . . . . . . . . 16 (∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8785, 86syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8850unieqi 4646 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
8987, 88syl6eqr 2865 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9084, 89sseqtrd 3845 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9146unissd 4663 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
929ad3antrrr 712 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = 𝑈)
9391, 92sseqtr4d 3846 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑋)
9490, 93eqssd 3822 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
95 unieq 4645 . . . . . . . . . . . . 13 (𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) → 𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9695rspceeqv 3527 . . . . . . . . . . . 12 ((ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9755, 94, 96syl2anc 575 . . . . . . . . . . 11 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9835, 97rexlimddv 3230 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9998ex 399 . . . . . . . . 9 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ⊆ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10022, 99syl5bir 234 . . . . . . . 8 ((𝜑𝑘𝐴) → (( (𝐹𝑘) ∖ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10121, 100mtod 189 . . . . . . 7 ((𝜑𝑘𝐴) → ¬ ( (𝐹𝑘) ∖ 𝐾) = ∅)
102 neq0 4138 . . . . . . 7 (¬ ( (𝐹𝑘) ∖ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
103101, 102sylib 209 . . . . . 6 ((𝜑𝑘𝐴) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
104 rexv 3421 . . . . . 6 (∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
105103, 104sylibr 225 . . . . 5 ((𝜑𝑘𝐴) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
10620, 105sylan2 582 . . . 4 ((𝜑𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
107106ralrimiva 3161 . . 3 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
108 eleq1 2880 . . . 4 (𝑦 = (𝑔𝑘) → (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
109108ac6num 9589 . . 3 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1103, 19, 107, 109syl3anc 1483 . 2 (𝜑 → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1111adantr 468 . . . 4 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝐴𝑉)
112 mptexg 6712 . . . 4 (𝐴𝑉 → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V)
113111, 112syl 17 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V)
114 fvex 6424 . . . . . . . 8 (𝐹𝑚) ∈ V
115114uniex 7186 . . . . . . 7 (𝐹𝑚) ∈ V
116115uniex 7186 . . . . . 6 (𝐹𝑚) ∈ V
117 fvex 6424 . . . . . 6 (𝑔𝑚) ∈ V
118116, 117ifex 4334 . . . . 5 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V
119118rgenw 3119 . . . 4 𝑚𝐴 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V
120 eqid 2813 . . . . 5 (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))
121120fnmpt 6234 . . . 4 (∀𝑚𝐴 if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) ∈ V → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
122119, 121mp1i 13 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
12358breq1d 4861 . . . . . . 7 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1𝑜 (𝐹𝑘) ≈ 1𝑜))
124123notbid 309 . . . . . 6 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1𝑜 ↔ ¬ (𝐹𝑘) ≈ 1𝑜))
125124ralrab 3571 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
126 iftrue 4292 . . . . . . . . . . 11 ( (𝐹𝑘) ≈ 1𝑜 → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
127126ad2antll 711 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
128103adantrr 699 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
12912adantl 469 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
130 simplrr 787 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ≈ 1𝑜)
131 en1b 8263 . . . . . . . . . . . . . . . 16 ( (𝐹𝑘) ≈ 1𝑜 (𝐹𝑘) = { (𝐹𝑘)})
132130, 131sylib 209 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) = { (𝐹𝑘)})
133129, 132eleqtrd 2894 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ { (𝐹𝑘)})
134 elsni 4394 . . . . . . . . . . . . . 14 (𝑦 ∈ { (𝐹𝑘)} → 𝑦 = (𝐹𝑘))
135133, 134syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 = (𝐹𝑘))
136 simpr 473 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
137135, 136eqeltrrd 2893 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
138128, 137exlimddv 2026 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
139138adantlr 697 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
140127, 139eqeltrd 2892 . . . . . . . . 9 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
141140a1d 25 . . . . . . . 8 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1𝑜)) → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
142141expr 446 . . . . . . 7 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘𝐴) → ( (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
143 pm2.27 42 . . . . . . . 8 (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
144 iffalse 4295 . . . . . . . . 9 (𝐹𝑘) ≈ 1𝑜 → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) = (𝑔𝑘))
145144eleq1d 2877 . . . . . . . 8 (𝐹𝑘) ≈ 1𝑜 → (if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
146143, 145sylibrd 250 . . . . . . 7 (𝐹𝑘) ≈ 1𝑜 → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
147142, 146pm2.61d1 172 . . . . . 6 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) ∧ 𝑘𝐴) → ((¬ (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
148147ralimdva 3157 . . . . 5 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) → (∀𝑘𝐴 (𝐹𝑘) ≈ 1𝑜 → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
149125, 148syl5bi 233 . . . 4 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V) → (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
150149impr 444 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
151 fneq1 6193 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴))
152 fveq1 6410 . . . . . . . . 9 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (𝑓𝑘) = ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))‘𝑘))
153 fveq2 6411 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
154153unieqd 4647 . . . . . . . . . . . 12 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
155154breq1d 4861 . . . . . . . . . . 11 (𝑚 = 𝑘 → ( (𝐹𝑚) ≈ 1𝑜 (𝐹𝑘) ≈ 1𝑜))
156154unieqd 4647 . . . . . . . . . . 11 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
157 fveq2 6411 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑔𝑚) = (𝑔𝑘))
158155, 156, 157ifbieq12d 4313 . . . . . . . . . 10 (𝑚 = 𝑘 → if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
159 fvex 6424 . . . . . . . . . . . . 13 (𝐹𝑘) ∈ V
160159uniex 7186 . . . . . . . . . . . 12 (𝐹𝑘) ∈ V
161160uniex 7186 . . . . . . . . . . 11 (𝐹𝑘) ∈ V
162 fvex 6424 . . . . . . . . . . 11 (𝑔𝑘) ∈ V
163161, 162ifex 4334 . . . . . . . . . 10 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ V
164158, 120, 163fvmpt 6506 . . . . . . . . 9 (𝑘𝐴 → ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚)))‘𝑘) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
165152, 164sylan9eq 2867 . . . . . . . 8 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → (𝑓𝑘) = if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)))
166165eleq1d 2877 . . . . . . 7 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
167166ralbidva 3180 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
168151, 167anbi12d 618 . . . . 5 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) ↔ ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
169168spcegv 3494 . . . 4 ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V → (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))))
1701693impib 1137 . . 3 (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) ∈ V ∧ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1𝑜, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1𝑜, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
171113, 122, 150, 170syl3anc 1483 . 2 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1𝑜} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
172110, 171exlimddv 2026 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384   = wceq 1637  wex 1859  wcel 2157  {cab 2799  wral 3103  wrex 3104  {crab 3107  Vcvv 3398  cdif 3773  cin 3775  wss 3776  c0 4123  ifcif 4286  𝒫 cpw 4358  {csn 4377   cuni 4637   ciun 4719   class class class wbr 4851  cmpt 4930  ccnv 5317  dom cdm 5318  ran crn 5319  cima 5321   Fn wfn 6099  wf 6100  cfv 6104  cmpt2 6879  1𝑜c1o 7792  Xcixp 8148  cen 8192  Fincfn 8195  cardccrd 9047  Compccmp 21407  UFLcufl 21921
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-8 2159  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2791  ax-rep 4971  ax-sep 4982  ax-nul 4990  ax-pow 5042  ax-pr 5103  ax-un 7182
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-mo 2635  df-eu 2638  df-clab 2800  df-cleq 2806  df-clel 2809  df-nfc 2944  df-ne 2986  df-ral 3108  df-rex 3109  df-reu 3110  df-rmo 3111  df-rab 3112  df-v 3400  df-sbc 3641  df-csb 3736  df-dif 3779  df-un 3781  df-in 3783  df-ss 3790  df-pss 3792  df-nul 4124  df-if 4287  df-pw 4360  df-sn 4378  df-pr 4380  df-tp 4382  df-op 4384  df-uni 4638  df-int 4677  df-iun 4721  df-br 4852  df-opab 4914  df-mpt 4931  df-tr 4954  df-id 5226  df-eprel 5231  df-po 5239  df-so 5240  df-fr 5277  df-se 5278  df-we 5279  df-xp 5324  df-rel 5325  df-cnv 5326  df-co 5327  df-dm 5328  df-rn 5329  df-res 5330  df-ima 5331  df-pred 5900  df-ord 5946  df-on 5947  df-lim 5948  df-suc 5949  df-iota 6067  df-fun 6106  df-fn 6107  df-f 6108  df-f1 6109  df-fo 6110  df-f1o 6111  df-fv 6112  df-isom 6113  df-riota 6838  df-ov 6880  df-oprab 6881  df-mpt2 6882  df-om 7299  df-1st 7401  df-2nd 7402  df-wrecs 7645  df-recs 7707  df-rdg 7745  df-1o 7799  df-oadd 7803  df-omul 7804  df-er 7982  df-map 8097  df-ixp 8149  df-en 8196  df-dom 8197  df-fin 8199  df-wdom 8706  df-card 9051  df-acn 9054  df-cmp 21408
This theorem is referenced by:  ptcmplem4  22076
  Copyright terms: Public domain W3C validator