This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑘 ) ∈ 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 biimtrrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) = ∅ → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ 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 biimtrid ⊢ ( ( 𝜑 ∧ 𝑔 : { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 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 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )