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

Theorem ptcmplem3 24043
Description: Lemma for ptcmp 24047. (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 5328 . . . 4 (𝐴𝑉 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V)
31, 2syl 17 . . 3 (𝜑 → {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ 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 24042 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
12 eldifi 4123 . . . . . . . 8 (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) → 𝑦 (𝐹𝑘))
13123ad2ant3 1132 . . . . . . 7 ((𝜑𝑦 ∈ V ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
1413rabssdv 4068 . . . . . 6 (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
1514ralrimivw 3140 . . . . 5 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
16 ss2iun 5011 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
1715, 16syl 17 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
18 ssnum 10072 . . . 4 (( 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘)) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
1911, 17, 18syl2anc 582 . . 3 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
20 elrabi 3674 . . . . 5 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} → 𝑘𝐴)
2110adantr 479 . . . . . . . 8 ((𝜑𝑘𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
22 ssdif0 4359 . . . . . . . . 9 ( (𝐹𝑘) ⊆ 𝐾 ↔ ( (𝐹𝑘) ∖ 𝐾) = ∅)
236ffvelcdmda 7087 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Comp)
2423adantr 479 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ∈ Comp)
25 ptcmplem3.8 . . . . . . . . . . . . . 14 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
2625ssrab3 4076 . . . . . . . . . . . . 13 𝐾 ⊆ (𝐹𝑘)
2726a1i 11 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 ⊆ (𝐹𝑘))
28 simpr 483 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ⊆ 𝐾)
29 uniss 4913 . . . . . . . . . . . . . 14 (𝐾 ⊆ (𝐹𝑘) → 𝐾 (𝐹𝑘))
3026, 29mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 (𝐹𝑘))
3128, 30eqssd 3996 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) = 𝐾)
32 eqid 2726 . . . . . . . . . . . . 13 (𝐹𝑘) = (𝐹𝑘)
3332cmpcov 23378 . . . . . . . . . . . 12 (((𝐹𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹𝑘) ∧ (𝐹𝑘) = 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
3424, 27, 31, 33syl3anc 1368 . . . . . . . . . . 11 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
35 elfpw 9388 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡𝐾𝑡 ∈ Fin))
3635simplbi 496 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡𝐾)
3736ad2antrl 726 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡𝐾)
3837sselda 3978 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → 𝑥𝐾)
39 imaeq2 6055 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4039eleq1d 2811 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → (((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈 ↔ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4140, 25elrab2 3683 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↔ (𝑥 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4241simprbi 495 . . . . . . . . . . . . . . . 16 (𝑥𝐾 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4338, 42syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4443fmpttd 7118 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)):𝑡𝑈)
4544frnd 6725 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
4635simprbi 495 . . . . . . . . . . . . . . 15 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
4746ad2antrl 726 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡 ∈ Fin)
48 eqid 2726 . . . . . . . . . . . . . . . 16 (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4948rnmpt 5951 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
50 abrexfi 9386 . . . . . . . . . . . . . . 15 (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)} ∈ Fin)
5149, 50eqeltrid 2830 . . . . . . . . . . . . . 14 (𝑡 ∈ Fin → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
5247, 51syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
53 elfpw 9388 . . . . . . . . . . . . 13 (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin))
5445, 52, 53sylanbrc 581 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
56 fveq2 6890 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
5756unieqd 4918 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
5855, 57eleq12d 2820 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
59 simpr 483 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓𝑋)
6059, 5eleqtrdi 2836 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
61 vex 3466 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
6261elixp 8922 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
6362simprbi 495 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
6460, 63syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
65 simp-4r 782 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑘𝐴)
6658, 64, 65rspcdva 3608 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ (𝐹𝑘))
67 simplrr 776 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝐹𝑘) = 𝑡)
6866, 67eleqtrd 2828 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ 𝑡)
69 eluni2 4909 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑘) ∈ 𝑡 ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
7068, 69sylib 217 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
71 fveq1 6889 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
7271eleq1d 2811 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑥 ↔ (𝑓𝑘) ∈ 𝑥))
73 eqid 2726 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
7473mptpreima 6239 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑥}
7572, 74elrab2 3683 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑥))
7675baib 534 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑋 → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7776ad2antlr 725 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) ∧ 𝑥𝑡) → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7877rexbidva 3167 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥))
7970, 78mpbird 256 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
80 eliun 4997 . . . . . . . . . . . . . . . . 17 (𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8179, 80sylibr 233 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8281ex 411 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑓𝑋𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8382ssrdv 3984 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8443ralrimiva 3136 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
85 dfiun2g 5030 . . . . . . . . . . . . . . . 16 (∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8684, 85syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8749unieqi 4917 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
8886, 87eqtr4di 2784 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8983, 88sseqtrd 4019 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9045unissd 4915 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
919ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = 𝑈)
9290, 91sseqtrrd 4020 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑋)
9389, 92eqssd 3996 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
94 unieq 4916 . . . . . . . . . . . . 13 (𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) → 𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9594rspceeqv 3629 . . . . . . . . . . . 12 ((ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9654, 93, 95syl2anc 582 . . . . . . . . . . 11 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9734, 96rexlimddv 3151 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9897ex 411 . . . . . . . . 9 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ⊆ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
9922, 98biimtrrid 242 . . . . . . . 8 ((𝜑𝑘𝐴) → (( (𝐹𝑘) ∖ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10021, 99mtod 197 . . . . . . 7 ((𝜑𝑘𝐴) → ¬ ( (𝐹𝑘) ∖ 𝐾) = ∅)
101 neq0 4345 . . . . . . 7 (¬ ( (𝐹𝑘) ∖ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
102100, 101sylib 217 . . . . . 6 ((𝜑𝑘𝐴) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
103 rexv 3490 . . . . . 6 (∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
104102, 103sylibr 233 . . . . 5 ((𝜑𝑘𝐴) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
10520, 104sylan2 591 . . . 4 ((𝜑𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
106105ralrimiva 3136 . . 3 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
107 eleq1 2814 . . . 4 (𝑦 = (𝑔𝑘) → (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
108107ac6num 10510 . . 3 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1093, 19, 106, 108syl3anc 1368 . 2 (𝜑 → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1101adantr 479 . . . 4 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝐴𝑉)
111110mptexd 7230 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V)
112 fvex 6903 . . . . . . . 8 (𝐹𝑚) ∈ V
113112uniex 7741 . . . . . . 7 (𝐹𝑚) ∈ V
114113uniex 7741 . . . . . 6 (𝐹𝑚) ∈ V
115 fvex 6903 . . . . . 6 (𝑔𝑚) ∈ V
116114, 115ifex 4573 . . . . 5 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V
117116rgenw 3055 . . . 4 𝑚𝐴 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V
118 eqid 2726 . . . . 5 (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))
119118fnmpt 6690 . . . 4 (∀𝑚𝐴 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
120117, 119mp1i 13 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
12157breq1d 5153 . . . . . . 7 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1o (𝐹𝑘) ≈ 1o))
122121notbid 317 . . . . . 6 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1o ↔ ¬ (𝐹𝑘) ≈ 1o))
123122ralrab 3686 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
124 iftrue 4529 . . . . . . . . . . 11 ( (𝐹𝑘) ≈ 1o → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
125124ad2antll 727 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
126102adantrr 715 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
12712adantl 480 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
128 simplrr 776 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ≈ 1o)
129 en1b 9048 . . . . . . . . . . . . . . . 16 ( (𝐹𝑘) ≈ 1o (𝐹𝑘) = { (𝐹𝑘)})
130128, 129sylib 217 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) = { (𝐹𝑘)})
131127, 130eleqtrd 2828 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ { (𝐹𝑘)})
132 elsni 4640 . . . . . . . . . . . . . 14 (𝑦 ∈ { (𝐹𝑘)} → 𝑦 = (𝐹𝑘))
133131, 132syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 = (𝐹𝑘))
134 simpr 483 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
135133, 134eqeltrrd 2827 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
136126, 135exlimddv 1931 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
137136adantlr 713 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
138125, 137eqeltrd 2826 . . . . . . . . 9 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
139138a1d 25 . . . . . . . 8 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
140139expr 455 . . . . . . 7 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ 𝑘𝐴) → ( (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
141 pm2.27 42 . . . . . . . 8 (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
142 iffalse 4532 . . . . . . . . 9 (𝐹𝑘) ≈ 1o → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝑔𝑘))
143142eleq1d 2811 . . . . . . . 8 (𝐹𝑘) ≈ 1o → (if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
144141, 143sylibrd 258 . . . . . . 7 (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
145140, 144pm2.61d1 180 . . . . . 6 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ 𝑘𝐴) → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
146145ralimdva 3157 . . . . 5 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) → (∀𝑘𝐴 (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
147123, 146biimtrid 241 . . . 4 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
148147impr 453 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
149 fneq1 6640 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴))
150 fveq1 6889 . . . . . . . . 9 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (𝑓𝑘) = ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))‘𝑘))
151 fveq2 6890 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
152151unieqd 4918 . . . . . . . . . . . 12 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
153152breq1d 5153 . . . . . . . . . . 11 (𝑚 = 𝑘 → ( (𝐹𝑚) ≈ 1o (𝐹𝑘) ≈ 1o))
154152unieqd 4918 . . . . . . . . . . 11 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
155 fveq2 6890 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑔𝑚) = (𝑔𝑘))
156153, 154, 155ifbieq12d 4551 . . . . . . . . . 10 (𝑚 = 𝑘 → if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
157 fvex 6903 . . . . . . . . . . . . 13 (𝐹𝑘) ∈ V
158157uniex 7741 . . . . . . . . . . . 12 (𝐹𝑘) ∈ V
159158uniex 7741 . . . . . . . . . . 11 (𝐹𝑘) ∈ V
160 fvex 6903 . . . . . . . . . . 11 (𝑔𝑘) ∈ V
161159, 160ifex 4573 . . . . . . . . . 10 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ V
162156, 118, 161fvmpt 6998 . . . . . . . . 9 (𝑘𝐴 → ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))‘𝑘) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
163150, 162sylan9eq 2786 . . . . . . . 8 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → (𝑓𝑘) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
164163eleq1d 2811 . . . . . . 7 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
165164ralbidva 3166 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
166149, 165anbi12d 630 . . . . 5 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) ↔ ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
167166spcegv 3582 . . . 4 ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V → (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))))
1681673impib 1113 . . 3 (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V ∧ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
169111, 120, 148, 168syl3anc 1368 . 2 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
170109, 169exlimddv 1931 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394   = wceq 1534  wex 1774  wcel 2099  {cab 2703  wral 3051  wrex 3060  {crab 3419  Vcvv 3462  cdif 3943  cin 3945  wss 3946  c0 4322  ifcif 4523  𝒫 cpw 4597  {csn 4623   cuni 4905   ciun 4993   class class class wbr 5143  cmpt 5226  ccnv 5671  dom cdm 5672  ran crn 5673  cima 5675   Fn wfn 6538  wf 6539  cfv 6543  cmpo 7415  1oc1o 8478  Xcixp 8915  cen 8960  Fincfn 8963  cardccrd 9968  Compccmp 23375  UFLcufl 23889
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2697  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7735
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2529  df-eu 2558  df-clab 2704  df-cleq 2718  df-clel 2803  df-nfc 2878  df-ne 2931  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3464  df-sbc 3776  df-csb 3892  df-dif 3949  df-un 3951  df-in 3953  df-ss 3963  df-pss 3966  df-nul 4323  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-op 4630  df-uni 4906  df-int 4947  df-iun 4995  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6302  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7369  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7866  df-1st 7992  df-2nd 7993  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-oadd 8489  df-omul 8490  df-er 8723  df-map 8846  df-ixp 8916  df-en 8964  df-dom 8965  df-fin 8967  df-wdom 9598  df-card 9972  df-acn 9975  df-cmp 23376
This theorem is referenced by:  ptcmplem4  24044
  Copyright terms: Public domain W3C validator