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

Theorem ptcmplem3 24062
Description: Lemma for ptcmp 24066. (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 5337 . . . 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 24061 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card)
12 eldifi 4131 . . . . . . . 8 (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) → 𝑦 (𝐹𝑘))
13123ad2ant3 1136 . . . . . . 7 ((𝜑𝑦 ∈ V ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
1413rabssdv 4075 . . . . . 6 (𝜑 → {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
1514ralrimivw 3150 . . . . 5 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘))
16 ss2iun 5010 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ (𝐹𝑘) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
1715, 16syl 17 . . . 4 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘))
18 ssnum 10079 . . . 4 (( 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘) ∈ dom card ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ⊆ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝐹𝑘)) → 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
1911, 17, 18syl2anc 584 . . 3 (𝜑 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card)
20 elrabi 3687 . . . . 5 (𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} → 𝑘𝐴)
2110adantr 480 . . . . . . . 8 ((𝜑𝑘𝐴) → ¬ ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
22 ssdif0 4366 . . . . . . . . 9 ( (𝐹𝑘) ⊆ 𝐾 ↔ ( (𝐹𝑘) ∖ 𝐾) = ∅)
236ffvelcdmda 7104 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ Comp)
2423adantr 480 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ∈ Comp)
25 ptcmplem3.8 . . . . . . . . . . . . . 14 𝐾 = {𝑢 ∈ (𝐹𝑘) ∣ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈}
2625ssrab3 4082 . . . . . . . . . . . . 13 𝐾 ⊆ (𝐹𝑘)
2726a1i 11 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 ⊆ (𝐹𝑘))
28 simpr 484 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) ⊆ 𝐾)
29 uniss 4915 . . . . . . . . . . . . . 14 (𝐾 ⊆ (𝐹𝑘) → 𝐾 (𝐹𝑘))
3026, 29mp1i 13 . . . . . . . . . . . . 13 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → 𝐾 (𝐹𝑘))
3128, 30eqssd 4001 . . . . . . . . . . . 12 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → (𝐹𝑘) = 𝐾)
32 eqid 2737 . . . . . . . . . . . . 13 (𝐹𝑘) = (𝐹𝑘)
3332cmpcov 23397 . . . . . . . . . . . 12 (((𝐹𝑘) ∈ Comp ∧ 𝐾 ⊆ (𝐹𝑘) ∧ (𝐹𝑘) = 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
3424, 27, 31, 33syl3anc 1373 . . . . . . . . . . 11 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑡 ∈ (𝒫 𝐾 ∩ Fin) (𝐹𝑘) = 𝑡)
35 elfpw 9394 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ↔ (𝑡𝐾𝑡 ∈ Fin))
3635simplbi 497 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡𝐾)
3736ad2antrl 728 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡𝐾)
3837sselda 3983 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → 𝑥𝐾)
39 imaeq2 6074 . . . . . . . . . . . . . . . . . . 19 (𝑢 = 𝑥 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4039eleq1d 2826 . . . . . . . . . . . . . . . . . 18 (𝑢 = 𝑥 → (((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑢) ∈ 𝑈 ↔ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4140, 25elrab2 3695 . . . . . . . . . . . . . . . . 17 (𝑥𝐾 ↔ (𝑥 ∈ (𝐹𝑘) ∧ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈))
4241simprbi 496 . . . . . . . . . . . . . . . 16 (𝑥𝐾 → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4338, 42syl 17 . . . . . . . . . . . . . . 15 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑥𝑡) → ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
4443fmpttd 7135 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)):𝑡𝑈)
4544frnd 6744 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
4635simprbi 496 . . . . . . . . . . . . . . 15 (𝑡 ∈ (𝒫 𝐾 ∩ Fin) → 𝑡 ∈ Fin)
4746ad2antrl 728 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑡 ∈ Fin)
48 eqid 2737 . . . . . . . . . . . . . . . 16 (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
4948rnmpt 5968 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
50 abrexfi 9392 . . . . . . . . . . . . . . 15 (𝑡 ∈ Fin → {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)} ∈ Fin)
5149, 50eqeltrid 2845 . . . . . . . . . . . . . 14 (𝑡 ∈ Fin → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
5247, 51syl 17 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin)
53 elfpw 9394 . . . . . . . . . . . . 13 (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ↔ (ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈 ∧ ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ Fin))
5445, 52, 53sylanbrc 583 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin))
55 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 → (𝑓𝑛) = (𝑓𝑘))
56 fveq2 6906 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑛 = 𝑘 → (𝐹𝑛) = (𝐹𝑘))
5756unieqd 4920 . . . . . . . . . . . . . . . . . . . . . 22 (𝑛 = 𝑘 (𝐹𝑛) = (𝐹𝑘))
5855, 57eleq12d 2835 . . . . . . . . . . . . . . . . . . . . 21 (𝑛 = 𝑘 → ((𝑓𝑛) ∈ (𝐹𝑛) ↔ (𝑓𝑘) ∈ (𝐹𝑘)))
59 simpr 484 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓𝑋)
6059, 5eleqtrdi 2851 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓X𝑛𝐴 (𝐹𝑛))
61 vex 3484 . . . . . . . . . . . . . . . . . . . . . . . 24 𝑓 ∈ V
6261elixp 8944 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓X𝑛𝐴 (𝐹𝑛) ↔ (𝑓 Fn 𝐴 ∧ ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛)))
6362simprbi 496 . . . . . . . . . . . . . . . . . . . . . 22 (𝑓X𝑛𝐴 (𝐹𝑛) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
6460, 63syl 17 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∀𝑛𝐴 (𝑓𝑛) ∈ (𝐹𝑛))
65 simp-4r 784 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑘𝐴)
6658, 64, 65rspcdva 3623 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ (𝐹𝑘))
67 simplrr 778 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝐹𝑘) = 𝑡)
6866, 67eleqtrd 2843 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (𝑓𝑘) ∈ 𝑡)
69 eluni2 4911 . . . . . . . . . . . . . . . . . . 19 ((𝑓𝑘) ∈ 𝑡 ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
7068, 69sylib 218 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥)
71 fveq1 6905 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤 = 𝑓 → (𝑤𝑘) = (𝑓𝑘))
7271eleq1d 2826 . . . . . . . . . . . . . . . . . . . . . 22 (𝑤 = 𝑓 → ((𝑤𝑘) ∈ 𝑥 ↔ (𝑓𝑘) ∈ 𝑥))
73 eqid 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑤𝑋 ↦ (𝑤𝑘)) = (𝑤𝑋 ↦ (𝑤𝑘))
7473mptpreima 6258 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑤𝑋 ∣ (𝑤𝑘) ∈ 𝑥}
7572, 74elrab2 3695 . . . . . . . . . . . . . . . . . . . . 21 (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑋 ∧ (𝑓𝑘) ∈ 𝑥))
7675baib 535 . . . . . . . . . . . . . . . . . . . 20 (𝑓𝑋 → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7776ad2antlr 727 . . . . . . . . . . . . . . . . . . 19 ((((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) ∧ 𝑥𝑡) → (𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ (𝑓𝑘) ∈ 𝑥))
7877rexbidva 3177 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → (∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 (𝑓𝑘) ∈ 𝑥))
7970, 78mpbird 257 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
80 eliun 4995 . . . . . . . . . . . . . . . . 17 (𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ↔ ∃𝑥𝑡 𝑓 ∈ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8179, 80sylibr 234 . . . . . . . . . . . . . . . 16 (((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) ∧ 𝑓𝑋) → 𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8281ex 412 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → (𝑓𝑋𝑓 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8382ssrdv 3989 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))
8443ralrimiva 3146 . . . . . . . . . . . . . . . 16 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈)
85 dfiun2g 5030 . . . . . . . . . . . . . . . 16 (∀𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) ∈ 𝑈 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8684, 85syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)})
8749unieqi 4919 . . . . . . . . . . . . . . 15 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) = {𝑓 ∣ ∃𝑥𝑡 𝑓 = ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)}
8886, 87eqtr4di 2795 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑥𝑡 ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥) = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
8983, 88sseqtrd 4020 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9045unissd 4917 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑈)
919ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = 𝑈)
9290, 91sseqtrrd 4021 . . . . . . . . . . . . 13 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ⊆ 𝑋)
9389, 92eqssd 4001 . . . . . . . . . . . 12 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
94 unieq 4918 . . . . . . . . . . . . 13 (𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) → 𝑧 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)))
9594rspceeqv 3645 . . . . . . . . . . . 12 ((ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥)) ∈ (𝒫 𝑈 ∩ Fin) ∧ 𝑋 = ran (𝑥𝑡 ↦ ((𝑤𝑋 ↦ (𝑤𝑘)) “ 𝑥))) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9654, 93, 95syl2anc 584 . . . . . . . . . . 11 ((((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) ∧ (𝑡 ∈ (𝒫 𝐾 ∩ Fin) ∧ (𝐹𝑘) = 𝑡)) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9734, 96rexlimddv 3161 . . . . . . . . . 10 (((𝜑𝑘𝐴) ∧ (𝐹𝑘) ⊆ 𝐾) → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧)
9897ex 412 . . . . . . . . 9 ((𝜑𝑘𝐴) → ( (𝐹𝑘) ⊆ 𝐾 → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
9922, 98biimtrrid 243 . . . . . . . 8 ((𝜑𝑘𝐴) → (( (𝐹𝑘) ∖ 𝐾) = ∅ → ∃𝑧 ∈ (𝒫 𝑈 ∩ Fin)𝑋 = 𝑧))
10021, 99mtod 198 . . . . . . 7 ((𝜑𝑘𝐴) → ¬ ( (𝐹𝑘) ∖ 𝐾) = ∅)
101 neq0 4352 . . . . . . 7 (¬ ( (𝐹𝑘) ∖ 𝐾) = ∅ ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
102100, 101sylib 218 . . . . . 6 ((𝜑𝑘𝐴) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
103 rexv 3509 . . . . . 6 (∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
104102, 103sylibr 234 . . . . 5 ((𝜑𝑘𝐴) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
10520, 104sylan2 593 . . . 4 ((𝜑𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}) → ∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
106105ralrimiva 3146 . . 3 (𝜑 → ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
107 eleq1 2829 . . . 4 (𝑦 = (𝑔𝑘) → (𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
108107ac6num 10519 . . 3 (({𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} ∈ V ∧ 𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} {𝑦 ∈ V ∣ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)} ∈ dom card ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}∃𝑦 ∈ V 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1093, 19, 106, 108syl3anc 1373 . 2 (𝜑 → ∃𝑔(𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
1101adantr 480 . . . 4 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → 𝐴𝑉)
111110mptexd 7244 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V)
112 fvex 6919 . . . . . . . 8 (𝐹𝑚) ∈ V
113112uniex 7761 . . . . . . 7 (𝐹𝑚) ∈ V
114113uniex 7761 . . . . . 6 (𝐹𝑚) ∈ V
115 fvex 6919 . . . . . 6 (𝑔𝑚) ∈ V
116114, 115ifex 4576 . . . . 5 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V
117116rgenw 3065 . . . 4 𝑚𝐴 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V
118 eqid 2737 . . . . 5 (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))
119118fnmpt 6708 . . . 4 (∀𝑚𝐴 if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) ∈ V → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
120117, 119mp1i 13 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴)
12157breq1d 5153 . . . . . . 7 (𝑛 = 𝑘 → ( (𝐹𝑛) ≈ 1o (𝐹𝑘) ≈ 1o))
122121notbid 318 . . . . . 6 (𝑛 = 𝑘 → (¬ (𝐹𝑛) ≈ 1o ↔ ¬ (𝐹𝑘) ≈ 1o))
123122ralrab 3699 . . . . 5 (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
124 iftrue 4531 . . . . . . . . . . 11 ( (𝐹𝑘) ≈ 1o → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
125124ad2antll 729 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝐹𝑘))
126102adantrr 717 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → ∃𝑦 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
12712adantl 481 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 (𝐹𝑘))
128 simplrr 778 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ≈ 1o)
129 en1b 9065 . . . . . . . . . . . . . . . 16 ( (𝐹𝑘) ≈ 1o (𝐹𝑘) = { (𝐹𝑘)})
130128, 129sylib 218 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) = { (𝐹𝑘)})
131127, 130eleqtrd 2843 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ { (𝐹𝑘)})
132 elsni 4643 . . . . . . . . . . . . . 14 (𝑦 ∈ { (𝐹𝑘)} → 𝑦 = (𝐹𝑘))
133131, 132syl 17 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 = (𝐹𝑘))
134 simpr 484 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾))
135133, 134eqeltrrd 2842 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) ∧ 𝑦 ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
136126, 135exlimddv 1935 . . . . . . . . . . 11 ((𝜑 ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
137136adantlr 715 . . . . . . . . . 10 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → (𝐹𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))
138125, 137eqeltrd 2841 . . . . . . . . 9 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
139138a1d 25 . . . . . . . 8 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ (𝑘𝐴 (𝐹𝑘) ≈ 1o)) → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
140139expr 456 . . . . . . 7 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ 𝑘𝐴) → ( (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
141 pm2.27 42 . . . . . . . 8 (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
142 iffalse 4534 . . . . . . . . 9 (𝐹𝑘) ≈ 1o → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) = (𝑔𝑘))
143142eleq1d 2826 . . . . . . . 8 (𝐹𝑘) ≈ 1o → (if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
144141, 143sylibrd 259 . . . . . . 7 (𝐹𝑘) ≈ 1o → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
145140, 144pm2.61d1 180 . . . . . 6 (((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) ∧ 𝑘𝐴) → ((¬ (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
146145ralimdva 3167 . . . . 5 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) → (∀𝑘𝐴 (𝐹𝑘) ≈ 1o → (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
147123, 146biimtrid 242 . . . 4 ((𝜑𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V) → (∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
148147impr 454 . . 3 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))
149 fneq1 6659 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (𝑓 Fn 𝐴 ↔ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴))
150 fveq1 6905 . . . . . . . . 9 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (𝑓𝑘) = ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))‘𝑘))
151 fveq2 6906 . . . . . . . . . . . . 13 (𝑚 = 𝑘 → (𝐹𝑚) = (𝐹𝑘))
152151unieqd 4920 . . . . . . . . . . . 12 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
153152breq1d 5153 . . . . . . . . . . 11 (𝑚 = 𝑘 → ( (𝐹𝑚) ≈ 1o (𝐹𝑘) ≈ 1o))
154152unieqd 4920 . . . . . . . . . . 11 (𝑚 = 𝑘 (𝐹𝑚) = (𝐹𝑘))
155 fveq2 6906 . . . . . . . . . . 11 (𝑚 = 𝑘 → (𝑔𝑚) = (𝑔𝑘))
156153, 154, 155ifbieq12d 4554 . . . . . . . . . 10 (𝑚 = 𝑘 → if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
157 fvex 6919 . . . . . . . . . . . . 13 (𝐹𝑘) ∈ V
158157uniex 7761 . . . . . . . . . . . 12 (𝐹𝑘) ∈ V
159158uniex 7761 . . . . . . . . . . 11 (𝐹𝑘) ∈ V
160 fvex 6919 . . . . . . . . . . 11 (𝑔𝑘) ∈ V
161159, 160ifex 4576 . . . . . . . . . 10 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ V
162156, 118, 161fvmpt 7016 . . . . . . . . 9 (𝑘𝐴 → ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚)))‘𝑘) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
163150, 162sylan9eq 2797 . . . . . . . 8 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → (𝑓𝑘) = if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)))
164163eleq1d 2826 . . . . . . 7 ((𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∧ 𝑘𝐴) → ((𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
165164ralbidva 3176 . . . . . 6 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → (∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾) ↔ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)))
166149, 165anbi12d 632 . . . . 5 (𝑓 = (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) → ((𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)) ↔ ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾))))
167166spcegv 3597 . . . 4 ((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V → (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))))
1681673impib 1117 . . 3 (((𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) ∈ V ∧ (𝑚𝐴 ↦ if( (𝐹𝑚) ≈ 1o, (𝐹𝑚), (𝑔𝑚))) Fn 𝐴 ∧ ∀𝑘𝐴 if( (𝐹𝑘) ≈ 1o, (𝐹𝑘), (𝑔𝑘)) ∈ ( (𝐹𝑘) ∖ 𝐾)) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
169111, 120, 148, 168syl3anc 1373 . 2 ((𝜑 ∧ (𝑔:{𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o}⟶V ∧ ∀𝑘 ∈ {𝑛𝐴 ∣ ¬ (𝐹𝑛) ≈ 1o} (𝑔𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾))) → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
170109, 169exlimddv 1935 1 (𝜑 → ∃𝑓(𝑓 Fn 𝐴 ∧ ∀𝑘𝐴 (𝑓𝑘) ∈ ( (𝐹𝑘) ∖ 𝐾)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395   = wceq 1540  wex 1779  wcel 2108  {cab 2714  wral 3061  wrex 3070  {crab 3436  Vcvv 3480  cdif 3948  cin 3950  wss 3951  c0 4333  ifcif 4525  𝒫 cpw 4600  {csn 4626   cuni 4907   ciun 4991   class class class wbr 5143  cmpt 5225  ccnv 5684  dom cdm 5685  ran crn 5686  cima 5688   Fn wfn 6556  wf 6557  cfv 6561  cmpo 7433  1oc1o 8499  Xcixp 8937  cen 8982  Fincfn 8985  cardccrd 9975  Compccmp 23394  UFLcufl 23908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-rep 5279  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-int 4947  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-se 5638  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-isom 6570  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8014  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-1o 8506  df-oadd 8510  df-omul 8511  df-er 8745  df-map 8868  df-ixp 8938  df-en 8986  df-dom 8987  df-fin 8989  df-wdom 9605  df-card 9979  df-acn 9982  df-cmp 23395
This theorem is referenced by:  ptcmplem4  24063
  Copyright terms: Public domain W3C validator