Metamath Proof Explorer


Theorem ptcmplem3

Description: Lemma for ptcmp . (Contributed by Mario Carneiro, 26-Aug-2015)

Ref Expression
Hypotheses 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 ptcmplem3 ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )

Proof

Step Hyp Ref Expression
1 ptcmp.1 𝑆 = ( 𝑘𝐴 , 𝑢 ∈ ( 𝐹𝑘 ) ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) )
2 ptcmp.2 𝑋 = X 𝑛𝐴 ( 𝐹𝑛 )
3 ptcmp.3 ( 𝜑𝐴𝑉 )
4 ptcmp.4 ( 𝜑𝐹 : 𝐴 ⟶ Comp )
5 ptcmp.5 ( 𝜑𝑋 ∈ ( UFL ∩ dom card ) )
6 ptcmplem2.5 ( 𝜑𝑈 ⊆ ran 𝑆 )
7 ptcmplem2.6 ( 𝜑𝑋 = 𝑈 )
8 ptcmplem2.7 ( 𝜑 → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 )
9 ptcmplem3.8 𝐾 = { 𝑢 ∈ ( 𝐹𝑘 ) ∣ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ∈ 𝑈 }
10 rabexg ( 𝐴𝑉 → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V )
11 3 10 syl ( 𝜑 → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V )
12 1 2 3 4 5 6 7 8 ptcmplem2 ( 𝜑 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card )
13 eldifi ( 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) → 𝑦 ( 𝐹𝑘 ) )
14 13 3ad2ant3 ( ( 𝜑𝑦 ∈ V ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → 𝑦 ( 𝐹𝑘 ) )
15 14 rabssdv ( 𝜑 → { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ ( 𝐹𝑘 ) )
16 15 ralrimivw ( 𝜑 → ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ ( 𝐹𝑘 ) )
17 ss2iun ( ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ ( 𝐹𝑘 ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
18 16 17 syl ( 𝜑 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
19 ssnum ( ( 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card ∧ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ⊆ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ∈ dom card )
20 12 18 19 syl2anc ( 𝜑 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ∈ dom card )
21 elrabi ( 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } → 𝑘𝐴 )
22 8 adantr ( ( 𝜑𝑘𝐴 ) → ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 )
23 ssdif0 ( ( 𝐹𝑘 ) ⊆ 𝐾 ↔ ( ( 𝐹𝑘 ) ∖ 𝐾 ) = ∅ )
24 4 ffvelrnda ( ( 𝜑𝑘𝐴 ) → ( 𝐹𝑘 ) ∈ Comp )
25 24 adantr ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → ( 𝐹𝑘 ) ∈ Comp )
26 9 ssrab3 𝐾 ⊆ ( 𝐹𝑘 )
27 26 a1i ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → 𝐾 ⊆ ( 𝐹𝑘 ) )
28 simpr ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → ( 𝐹𝑘 ) ⊆ 𝐾 )
29 uniss ( 𝐾 ⊆ ( 𝐹𝑘 ) → 𝐾 ( 𝐹𝑘 ) )
30 26 29 mp1i ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → 𝐾 ( 𝐹𝑘 ) )
31 28 30 eqssd ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → ( 𝐹𝑘 ) = 𝐾 )
32 eqid ( 𝐹𝑘 ) = ( 𝐹𝑘 )
33 32 cmpcov ( ( ( 𝐹𝑘 ) ∈ Comp ∧ 𝐾 ⊆ ( 𝐹𝑘 ) ∧ ( 𝐹𝑘 ) = 𝐾 ) → ∃ 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ( 𝐹𝑘 ) = 𝑡 )
34 25 27 31 33 syl3anc ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → ∃ 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ( 𝐹𝑘 ) = 𝑡 )
35 elfpw ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ↔ ( 𝑡𝐾𝑡 ∈ Fin ) )
36 35 simplbi ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) → 𝑡𝐾 )
37 36 ad2antrl ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑡𝐾 )
38 37 sselda ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑥𝑡 ) → 𝑥𝐾 )
39 imaeq2 ( 𝑢 = 𝑥 → ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
40 39 eleq1d ( 𝑢 = 𝑥 → ( ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑢 ) ∈ 𝑈 ↔ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 ) )
41 40 9 elrab2 ( 𝑥𝐾 ↔ ( 𝑥 ∈ ( 𝐹𝑘 ) ∧ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 ) )
42 41 simprbi ( 𝑥𝐾 → ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
43 38 42 syl ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑥𝑡 ) → ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
44 43 fmpttd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) : 𝑡𝑈 )
45 44 frnd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑈 )
46 35 simprbi ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) → 𝑡 ∈ Fin )
47 46 ad2antrl ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑡 ∈ Fin )
48 eqid ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) = ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
49 48 rnmpt ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) = { 𝑓 ∣ ∃ 𝑥𝑡 𝑓 = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) }
50 abrexfi ( 𝑡 ∈ Fin → { 𝑓 ∣ ∃ 𝑥𝑡 𝑓 = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) } ∈ Fin )
51 49 50 eqeltrid ( 𝑡 ∈ Fin → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ Fin )
52 47 51 syl ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ Fin )
53 elfpw ( ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑈 ∧ ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ Fin ) )
54 45 52 53 sylanbrc ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) )
55 fveq2 ( 𝑛 = 𝑘 → ( 𝑓𝑛 ) = ( 𝑓𝑘 ) )
56 fveq2 ( 𝑛 = 𝑘 → ( 𝐹𝑛 ) = ( 𝐹𝑘 ) )
57 56 unieqd ( 𝑛 = 𝑘 ( 𝐹𝑛 ) = ( 𝐹𝑘 ) )
58 55 57 eleq12d ( 𝑛 = 𝑘 → ( ( 𝑓𝑛 ) ∈ ( 𝐹𝑛 ) ↔ ( 𝑓𝑘 ) ∈ ( 𝐹𝑘 ) ) )
59 simpr ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → 𝑓𝑋 )
60 59 2 eleqtrdi ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → 𝑓X 𝑛𝐴 ( 𝐹𝑛 ) )
61 vex 𝑓 ∈ V
62 61 elixp ( 𝑓X 𝑛𝐴 ( 𝐹𝑛 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑛𝐴 ( 𝑓𝑛 ) ∈ ( 𝐹𝑛 ) ) )
63 62 simprbi ( 𝑓X 𝑛𝐴 ( 𝐹𝑛 ) → ∀ 𝑛𝐴 ( 𝑓𝑛 ) ∈ ( 𝐹𝑛 ) )
64 60 63 syl ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ∀ 𝑛𝐴 ( 𝑓𝑛 ) ∈ ( 𝐹𝑛 ) )
65 simp-4r ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → 𝑘𝐴 )
66 58 64 65 rspcdva ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ( 𝑓𝑘 ) ∈ ( 𝐹𝑘 ) )
67 simplrr ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ( 𝐹𝑘 ) = 𝑡 )
68 66 67 eleqtrd ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ( 𝑓𝑘 ) ∈ 𝑡 )
69 eluni2 ( ( 𝑓𝑘 ) ∈ 𝑡 ↔ ∃ 𝑥𝑡 ( 𝑓𝑘 ) ∈ 𝑥 )
70 68 69 sylib ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ∃ 𝑥𝑡 ( 𝑓𝑘 ) ∈ 𝑥 )
71 fveq1 ( 𝑤 = 𝑓 → ( 𝑤𝑘 ) = ( 𝑓𝑘 ) )
72 71 eleq1d ( 𝑤 = 𝑓 → ( ( 𝑤𝑘 ) ∈ 𝑥 ↔ ( 𝑓𝑘 ) ∈ 𝑥 ) )
73 eqid ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) = ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) )
74 73 mptpreima ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) = { 𝑤𝑋 ∣ ( 𝑤𝑘 ) ∈ 𝑥 }
75 72 74 elrab2 ( 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓𝑋 ∧ ( 𝑓𝑘 ) ∈ 𝑥 ) )
76 75 baib ( 𝑓𝑋 → ( 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓𝑘 ) ∈ 𝑥 ) )
77 76 ad2antlr ( ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) ∧ 𝑥𝑡 ) → ( 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ↔ ( 𝑓𝑘 ) ∈ 𝑥 ) )
78 77 rexbidva ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ( ∃ 𝑥𝑡 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ↔ ∃ 𝑥𝑡 ( 𝑓𝑘 ) ∈ 𝑥 ) )
79 70 78 mpbird ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → ∃ 𝑥𝑡 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
80 eliun ( 𝑓 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ↔ ∃ 𝑥𝑡 𝑓 ∈ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
81 79 80 sylibr ( ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) ∧ 𝑓𝑋 ) → 𝑓 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
82 81 ex ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ( 𝑓𝑋𝑓 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) )
83 82 ssrdv ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑋 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) )
84 43 ralrimiva ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ∀ 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 )
85 dfiun2g ( ∀ 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ∈ 𝑈 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) = { 𝑓 ∣ ∃ 𝑥𝑡 𝑓 = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) } )
86 84 85 syl ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) = { 𝑓 ∣ ∃ 𝑥𝑡 𝑓 = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) } )
87 49 unieqi ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) = { 𝑓 ∣ ∃ 𝑥𝑡 𝑓 = ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) }
88 86 87 eqtr4di ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑥𝑡 ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) = ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) )
89 83 88 sseqtrd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑋 ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) )
90 45 unissd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑈 )
91 7 ad3antrrr ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑋 = 𝑈 )
92 90 91 sseqtrrd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ⊆ 𝑋 )
93 89 92 eqssd ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → 𝑋 = ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) )
94 unieq ( 𝑧 = ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) → 𝑧 = ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) )
95 94 rspceeqv ( ( ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑋 = ran ( 𝑥𝑡 ↦ ( ( 𝑤𝑋 ↦ ( 𝑤𝑘 ) ) “ 𝑥 ) ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 )
96 54 93 95 syl2anc ( ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) ∧ ( 𝑡 ∈ ( 𝒫 𝐾 ∩ Fin ) ∧ ( 𝐹𝑘 ) = 𝑡 ) ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 )
97 34 96 rexlimddv ( ( ( 𝜑𝑘𝐴 ) ∧ ( 𝐹𝑘 ) ⊆ 𝐾 ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 )
98 97 ex ( ( 𝜑𝑘𝐴 ) → ( ( 𝐹𝑘 ) ⊆ 𝐾 → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 ) )
99 23 98 syl5bir ( ( 𝜑𝑘𝐴 ) → ( ( ( 𝐹𝑘 ) ∖ 𝐾 ) = ∅ → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = 𝑧 ) )
100 22 99 mtod ( ( 𝜑𝑘𝐴 ) → ¬ ( ( 𝐹𝑘 ) ∖ 𝐾 ) = ∅ )
101 neq0 ( ¬ ( ( 𝐹𝑘 ) ∖ 𝐾 ) = ∅ ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
102 100 101 sylib ( ( 𝜑𝑘𝐴 ) → ∃ 𝑦 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
103 rexv ( ∃ 𝑦 ∈ V 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ ∃ 𝑦 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
104 102 103 sylibr ( ( 𝜑𝑘𝐴 ) → ∃ 𝑦 ∈ V 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
105 21 104 sylan2 ( ( 𝜑𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) → ∃ 𝑦 ∈ V 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
106 105 ralrimiva ( 𝜑 → ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∃ 𝑦 ∈ V 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
107 eleq1 ( 𝑦 = ( 𝑔𝑘 ) → ( 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
108 107 ac6num ( ( { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V ∧ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } { 𝑦 ∈ V ∣ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) } ∈ dom card ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∃ 𝑦 ∈ V 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ∃ 𝑔 ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
109 11 20 106 108 syl3anc ( 𝜑 → ∃ 𝑔 ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
110 3 adantr ( ( 𝜑 ∧ ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) → 𝐴𝑉 )
111 110 mptexd ( ( 𝜑 ∧ ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) → ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ∈ V )
112 fvex ( 𝐹𝑚 ) ∈ V
113 112 uniex ( 𝐹𝑚 ) ∈ V
114 113 uniex ( 𝐹𝑚 ) ∈ V
115 fvex ( 𝑔𝑚 ) ∈ V
116 114 115 ifex if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ∈ V
117 116 rgenw 𝑚𝐴 if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ∈ V
118 eqid ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) )
119 118 fnmpt ( ∀ 𝑚𝐴 if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ∈ V → ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 )
120 117 119 mp1i ( ( 𝜑 ∧ ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) → ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 )
121 57 breq1d ( 𝑛 = 𝑘 → ( ( 𝐹𝑛 ) ≈ 1o ( 𝐹𝑘 ) ≈ 1o ) )
122 121 notbid ( 𝑛 = 𝑘 → ( ¬ ( 𝐹𝑛 ) ≈ 1o ↔ ¬ ( 𝐹𝑘 ) ≈ 1o ) )
123 122 ralrab ( ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ ∀ 𝑘𝐴 ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
124 iftrue ( ( 𝐹𝑘 ) ≈ 1o → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) = ( 𝐹𝑘 ) )
125 124 ad2antll ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) = ( 𝐹𝑘 ) )
126 102 adantrr ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → ∃ 𝑦 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
127 13 adantl ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → 𝑦 ( 𝐹𝑘 ) )
128 simplrr ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ( 𝐹𝑘 ) ≈ 1o )
129 en1b ( ( 𝐹𝑘 ) ≈ 1o ( 𝐹𝑘 ) = { ( 𝐹𝑘 ) } )
130 128 129 sylib ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ( 𝐹𝑘 ) = { ( 𝐹𝑘 ) } )
131 127 130 eleqtrd ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → 𝑦 ∈ { ( 𝐹𝑘 ) } )
132 elsni ( 𝑦 ∈ { ( 𝐹𝑘 ) } → 𝑦 = ( 𝐹𝑘 ) )
133 131 132 syl ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → 𝑦 = ( 𝐹𝑘 ) )
134 simpr ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
135 133 134 eqeltrrd ( ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) ∧ 𝑦 ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ( 𝐹𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
136 126 135 exlimddv ( ( 𝜑 ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → ( 𝐹𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
137 136 adantlr ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → ( 𝐹𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
138 125 137 eqeltrd ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
139 138 a1d ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ ( 𝑘𝐴 ( 𝐹𝑘 ) ≈ 1o ) ) → ( ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
140 139 expr ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ 𝑘𝐴 ) → ( ( 𝐹𝑘 ) ≈ 1o → ( ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) )
141 pm2.27 ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
142 iffalse ( ¬ ( 𝐹𝑘 ) ≈ 1o → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) = ( 𝑔𝑘 ) )
143 142 eleq1d ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
144 141 143 sylibrd ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
145 140 144 pm2.61d1 ( ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) ∧ 𝑘𝐴 ) → ( ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
146 145 ralimdva ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) → ( ∀ 𝑘𝐴 ( ¬ ( 𝐹𝑘 ) ≈ 1o → ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
147 123 146 syl5bi ( ( 𝜑𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ) → ( ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) → ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
148 147 impr ( ( 𝜑 ∧ ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) → ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) )
149 fneq1 ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) → ( 𝑓 Fn 𝐴 ↔ ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 ) )
150 fveq1 ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) → ( 𝑓𝑘 ) = ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ‘ 𝑘 ) )
151 fveq2 ( 𝑚 = 𝑘 → ( 𝐹𝑚 ) = ( 𝐹𝑘 ) )
152 151 unieqd ( 𝑚 = 𝑘 ( 𝐹𝑚 ) = ( 𝐹𝑘 ) )
153 152 breq1d ( 𝑚 = 𝑘 → ( ( 𝐹𝑚 ) ≈ 1o ( 𝐹𝑘 ) ≈ 1o ) )
154 152 unieqd ( 𝑚 = 𝑘 ( 𝐹𝑚 ) = ( 𝐹𝑘 ) )
155 fveq2 ( 𝑚 = 𝑘 → ( 𝑔𝑚 ) = ( 𝑔𝑘 ) )
156 153 154 155 ifbieq12d ( 𝑚 = 𝑘 → if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) = if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) )
157 fvex ( 𝐹𝑘 ) ∈ V
158 157 uniex ( 𝐹𝑘 ) ∈ V
159 158 uniex ( 𝐹𝑘 ) ∈ V
160 fvex ( 𝑔𝑘 ) ∈ V
161 159 160 ifex if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ V
162 156 118 161 fvmpt ( 𝑘𝐴 → ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ‘ 𝑘 ) = if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) )
163 150 162 sylan9eq ( ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ∧ 𝑘𝐴 ) → ( 𝑓𝑘 ) = if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) )
164 163 eleq1d ( ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ∧ 𝑘𝐴 ) → ( ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
165 164 ralbidva ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) → ( ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ↔ ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
166 149 165 anbi12d ( 𝑓 = ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) → ( ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ↔ ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) )
167 166 spcegv ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ∈ V → ( ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) )
168 167 3impib ( ( ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) ∈ V ∧ ( 𝑚𝐴 ↦ if ( ( 𝐹𝑚 ) ≈ 1o , ( 𝐹𝑚 ) , ( 𝑔𝑚 ) ) ) Fn 𝐴 ∧ ∀ 𝑘𝐴 if ( ( 𝐹𝑘 ) ≈ 1o , ( 𝐹𝑘 ) , ( 𝑔𝑘 ) ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
169 111 120 148 168 syl3anc ( ( 𝜑 ∧ ( 𝑔 : { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⟶ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝑔𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) ) → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )
170 109 169 exlimddv ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘𝐴 ( 𝑓𝑘 ) ∈ ( ( 𝐹𝑘 ) ∖ 𝐾 ) ) )