Metamath Proof Explorer

Theorem ptcmplem4

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 ptcmplem4 ¬ 𝜑

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 1 2 3 4 5 6 7 8 9 ptcmplem3 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
11 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑓 Fn 𝐴 )
12 eldifi ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
13 12 ralimi ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
14 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑘 ) )
15 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
16 15 unieqd ⊢ ( 𝑛 = 𝑘 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
17 14 16 eleq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
18 17 cbvralvw ⊢ ( ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
19 13 18 sylibr ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
20 19 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
21 vex ⊢ 𝑓 ∈ V
22 21 elixp ⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
23 11 20 22 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
24 23 2 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑓 ∈ 𝑋 )
25 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑋 = ∪ 𝑈 )
26 24 25 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑓 ∈ ∪ 𝑈 )
27 eluni2 ⊢ ( 𝑓 ∈ ∪ 𝑈 ↔ ∃ 𝑣 ∈ 𝑈 𝑓 ∈ 𝑣 )
28 26 27 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∃ 𝑣 ∈ 𝑈 𝑓 ∈ 𝑣 )
29 simplrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑓 ∈ 𝑣 )
30 29 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑓 ∈ 𝑣 )
31 simprr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
32 30 31 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑓 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
33 fveq1 ⊢ ( 𝑤 = 𝑓 → ( 𝑤 ‘ 𝑘 ) = ( 𝑓 ‘ 𝑘 ) )
34 33 eleq1d ⊢ ( 𝑤 = 𝑓 → ( ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 ↔ ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ) )
35 eqid ⊢ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) = ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) )
36 35 mptpreima ⊢ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) = { 𝑤 ∈ 𝑋 ∣ ( 𝑤 ‘ 𝑘 ) ∈ 𝑢 }
37 34 36 elrab2 ⊢ ( 𝑓 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ↔ ( 𝑓 ∈ 𝑋 ∧ ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ) )
38 37 simprbi ⊢ ( 𝑓 ∈ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 )
39 32 38 syl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 )
40 simprl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) )
41 simplrl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑣 ∈ 𝑈 )
42 41 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑣 ∈ 𝑈 )
43 31 42 eqeltrrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 )
44 rabid ⊢ ( 𝑢 ∈ { 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∣ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 } ↔ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 ) )
45 40 43 44 sylanbrc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑢 ∈ { 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∣ ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ∈ 𝑈 } )
46 45 9 eleqtrrdi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → 𝑢 ∈ 𝐾 )
47 elunii ⊢ ( ( ( 𝑓 ‘ 𝑘 ) ∈ 𝑢 ∧ 𝑢 ∈ 𝐾 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
48 39 46 47 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) ∧ 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) ) ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
49 48 rexlimdvaa ⊢ ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ ( 𝑘 ∈ 𝐴 ∧ ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) )
50 49 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) ) )
51 50 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) ) )
52 51 ex ⊢ ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) → ( ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) ) ) )
53 52 com23 ⊢ ( ( 𝜑 ∧ 𝑓 Fn 𝐴 ) → ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ( ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) → ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) ) ) )
54 53 impr ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ( ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) → ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) ) )
55 54 imp ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) )
56 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → 𝑈 ⊆ ran 𝑆 )
57 56 sselda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ 𝑣 ∈ 𝑈 ) → 𝑣 ∈ ran 𝑆 )
58 57 adantrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → 𝑣 ∈ ran 𝑆 )
59 1 rnmpo ⊢ ran 𝑆 = { 𝑣 ∣ ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) }
60 58 59 eleqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → 𝑣 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) } )
61 abid ⊢ ( 𝑣 ∈ { 𝑣 ∣ ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) } ↔ ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
62 60 61 sylib ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) )
63 rexim ⊢ ( ∀ 𝑘 ∈ 𝐴 ( ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) → ( ∃ 𝑘 ∈ 𝐴 ∃ 𝑢 ∈ ( 𝐹 ‘ 𝑘 ) 𝑣 = ( ◡ ( 𝑤 ∈ 𝑋 ↦ ( 𝑤 ‘ 𝑘 ) ) “ 𝑢 ) → ∃ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ) )
64 55 62 63 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) ∧ ( 𝑣 ∈ 𝑈 ∧ 𝑓 ∈ 𝑣 ) ) → ∃ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
65 28 64 rexlimddv ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∃ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
66 eldifn ⊢ ( ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ¬ ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
67 66 ralimi ⊢ ( ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) → ∀ 𝑘 ∈ 𝐴 ¬ ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
68 67 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ∀ 𝑘 ∈ 𝐴 ¬ ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
69 ralnex ⊢ ( ∀ 𝑘 ∈ 𝐴 ¬ ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 ↔ ¬ ∃ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
70 68 69 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) ) → ¬ ∃ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ 𝐾 )
71 65 70 pm2.65da ⊢ ( 𝜑 → ¬ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
72 71 nexdv ⊢ ( 𝜑 → ¬ ∃ 𝑓 ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ ∪ 𝐾 ) ) )
73 10 72 pm2.65i ⊢ ¬ 𝜑