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

Metamath Proof Explorer

Theorem ptcmplem2

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 ) 𝑋 = ∪ 𝑧 )
Assertion ptcmplem2 ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )

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 0ss ⊢ ∅ ⊆ 𝑈
10 0fi ⊢ ∅ ∈ Fin
11 elfpw ⊢ ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ↔ ( ∅ ⊆ 𝑈 ∧ ∅ ∈ Fin ) )
12 9 10 11 mpbir2an ⊢ ∅ ∈ ( 𝒫 𝑈 ∩ Fin )
13 unieq ⊢ ( 𝑧 = ∅ → ∪ 𝑧 = ∪ ∅ )
14 uni0 ⊢ ∪ ∅ = ∅
15 13 14 eqtrdi ⊢ ( 𝑧 = ∅ → ∪ 𝑧 = ∅ )
16 15 rspceeqv ⊢ ( ( ∅ ∈ ( 𝒫 𝑈 ∩ Fin ) ∧ 𝑋 = ∅ ) → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
17 12 16 mpan ⊢ ( 𝑋 = ∅ → ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 )
18 17 necon3bi ⊢ ( ¬ ∃ 𝑧 ∈ ( 𝒫 𝑈 ∩ Fin ) 𝑋 = ∪ 𝑧 → 𝑋 ≠ ∅ )
19 8 18 syl ⊢ ( 𝜑 → 𝑋 ≠ ∅ )
20 n0 ⊢ ( 𝑋 ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ 𝑋 )
21 19 20 sylib ⊢ ( 𝜑 → ∃ 𝑓 𝑓 ∈ 𝑋 )
22 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐹 ‘ 𝑛 ) = ( 𝐹 ‘ 𝑘 ) )
23 22 unieqd ⊢ ( 𝑛 = 𝑘 → ∪ ( 𝐹 ‘ 𝑛 ) = ∪ ( 𝐹 ‘ 𝑘 ) )
24 23 cbvixpv ⊢ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 )
25 2 24 eqtri ⊢ 𝑋 = X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 )
26 5 elin2d ⊢ ( 𝜑 → 𝑋 ∈ dom card )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ∈ dom card )
28 25 27 eqeltrrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
29 ssrab2 ⊢ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴
30 19 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑋 ≠ ∅ )
31 25 30 eqnetrrid ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ )
32 eqid ⊢ ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) = ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) )
33 32 resixpfo ⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴 ∧ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) → ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) )
34 29 31 33 sylancr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) )
35 fonum ⊢ ( ( X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ∧ ( 𝑔 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↦ ( 𝑔 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) : X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) –onto→ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
36 28 34 35 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
37 vex ⊢ 𝑔 ∈ V
38 difexg ⊢ ( 𝑔 ∈ V → ( 𝑔 ∖ 𝑓 ) ∈ V )
39 37 38 mp1i ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∖ 𝑓 ) ∈ V )
40 dmexg ⊢ ( ( 𝑔 ∖ 𝑓 ) ∈ V → dom ( 𝑔 ∖ 𝑓 ) ∈ V )
41 uniexg ⊢ ( dom ( 𝑔 ∖ 𝑓 ) ∈ V → ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V )
42 39 40 41 3syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V )
43 42 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑔 ∈ 𝑋 ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V )
44 eqid ⊢ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) = ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) )
45 44 fnmpt ⊢ ( ∀ 𝑔 ∈ 𝑋 ∪ dom ( 𝑔 ∖ 𝑓 ) ∈ V → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 )
46 43 45 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 )
47 dffn4 ⊢ ( ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) Fn 𝑋 ↔ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
48 46 47 sylib ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
49 fonum ⊢ ( ( 𝑋 ∈ dom card ∧ ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) : 𝑋 –onto→ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) → ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card )
50 27 48 49 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card )
51 ssdif0 ⊢ ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ↔ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ )
52 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } )
53 simpr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ 𝑋 )
54 53 25 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) )
55 vex ⊢ 𝑓 ∈ V
56 55 elixp ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
57 56 simprbi ⊢ ( 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
58 54 57 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑘 ∈ 𝐴 ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
59 58 r19.21bi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑘 ) ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
60 59 snssd ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → { ( 𝑓 ‘ 𝑘 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → { ( 𝑓 ‘ 𝑘 ) } ⊆ ∪ ( 𝐹 ‘ 𝑘 ) )
62 52 61 eqssd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) = { ( 𝑓 ‘ 𝑘 ) } )
63 fvex ⊢ ( 𝑓 ‘ 𝑘 ) ∈ V
64 63 ensn1 ⊢ { ( 𝑓 ‘ 𝑘 ) } ≈ 1o
65 62 64 eqbrtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } ) → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o )
66 65 ex ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ∪ ( 𝐹 ‘ 𝑘 ) ⊆ { ( 𝑓 ‘ 𝑘 ) } → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) )
67 51 66 biimtrrid ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ → ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) )
68 67 con3d ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ ) )
69 neq0 ⊢ ( ¬ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) )
70 68 69 imbitrdi ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) )
71 eldifi ⊢ ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
72 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) )
73 iftrue ⊢ ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = 𝑥 )
74 73 23 eleq12d ⊢ ( 𝑛 = 𝑘 → ( if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) )
75 72 74 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
76 53 2 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
77 55 elixp ⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
78 77 simprbi ⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
79 76 78 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
80 79 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑛 ∈ 𝐴 ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
81 80 r19.21bi ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
82 iffalse ⊢ ( ¬ 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = ( 𝑓 ‘ 𝑛 ) )
83 82 eleq1d ⊢ ( ¬ 𝑛 = 𝑘 → ( if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ↔ ( 𝑓 ‘ 𝑛 ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
84 81 83 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → ( ¬ 𝑛 = 𝑘 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
85 75 84 pm2.61d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) ∧ 𝑛 ∈ 𝐴 ) → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
86 85 ralrimiva ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) )
87 3 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → 𝐴 ∈ 𝑉 )
88 mptelixpg ⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
89 87 88 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) ↔ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ ∪ ( 𝐹 ‘ 𝑛 ) ) )
90 86 89 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) )
91 90 2 eleqtrrdi ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 )
92 71 91 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 )
93 unisnv ⊢ ∪ { 𝑘 } = 𝑘
94 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑘 ∈ 𝐴 )
95 eleq1w ⊢ ( 𝑚 = 𝑘 → ( 𝑚 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
96 94 95 syl5ibrcom ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 → 𝑚 ∈ 𝐴 ) )
97 96 pm4.71rd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘 ) ) )
98 equequ1 ⊢ ( 𝑛 = 𝑚 → ( 𝑛 = 𝑘 ↔ 𝑚 = 𝑘 ) )
99 fveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝑓 ‘ 𝑛 ) = ( 𝑓 ‘ 𝑚 ) )
100 98 99 ifbieq2d ⊢ ( 𝑛 = 𝑚 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) )
101 eqid ⊢ ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) )
102 vex ⊢ 𝑥 ∈ V
103 fvex ⊢ ( 𝑓 ‘ 𝑚 ) ∈ V
104 102 103 ifex ⊢ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ∈ V
105 100 101 104 fvmpt ⊢ ( 𝑚 ∈ 𝐴 → ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) )
106 105 neeq1d ⊢ ( 𝑚 ∈ 𝐴 → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) )
107 106 adantl ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) )
108 iffalse ⊢ ( ¬ 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) = ( 𝑓 ‘ 𝑚 ) )
109 108 necon1ai ⊢ ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) → 𝑚 = 𝑘 )
110 eldifsni ⊢ ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) )
111 110 ad2antlr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) )
112 iftrue ⊢ ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) = 𝑥 )
113 fveq2 ⊢ ( 𝑚 = 𝑘 → ( 𝑓 ‘ 𝑚 ) = ( 𝑓 ‘ 𝑘 ) )
114 112 113 neeq12d ⊢ ( 𝑚 = 𝑘 → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑥 ≠ ( 𝑓 ‘ 𝑘 ) ) )
115 111 114 syl5ibrcom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ) )
116 109 115 impbid2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑚 ) ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑚 = 𝑘 ) )
117 107 116 bitrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) ∧ 𝑚 ∈ 𝐴 ) → ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ↔ 𝑚 = 𝑘 ) )
118 117 pm5.32da ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) ↔ ( 𝑚 ∈ 𝐴 ∧ 𝑚 = 𝑘 ) ) )
119 97 118 bitr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) ) )
120 119 abbidv ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑚 ∣ 𝑚 = 𝑘 } = { 𝑚 ∣ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) } )
121 df-sn ⊢ { 𝑘 } = { 𝑚 ∣ 𝑚 = 𝑘 }
122 df-rab ⊢ { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } = { 𝑚 ∣ ( 𝑚 ∈ 𝐴 ∧ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) ) }
123 120 121 122 3eqtr4g ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑘 } = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } )
124 fvex ⊢ ( 𝑓 ‘ 𝑛 ) ∈ V
125 102 124 ifex ⊢ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V
126 125 rgenw ⊢ ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V
127 101 fnmpt ⊢ ( ∀ 𝑛 ∈ 𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ∈ V → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 )
128 126 127 mp1i ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 )
129 ixpfn ⊢ ( 𝑓 ∈ X 𝑛 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑛 ) → 𝑓 Fn 𝐴 )
130 76 129 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝑓 Fn 𝐴 )
131 130 ad2antrr ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑓 Fn 𝐴 )
132 fndmdif ⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) Fn 𝐴 ∧ 𝑓 Fn 𝐴 ) → dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } )
133 128 131 132 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚 ∈ 𝐴 ∣ ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓 ‘ 𝑚 ) } )
134 123 133 eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → { 𝑘 } = dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
135 134 unieqd ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ∪ { 𝑘 } = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
136 93 135 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → 𝑘 = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
137 difeq1 ⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → ( 𝑔 ∖ 𝑓 ) = ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
138 137 dmeqd ⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → dom ( 𝑔 ∖ 𝑓 ) = dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
139 138 unieqd ⊢ ( 𝑔 = ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) → ∪ dom ( 𝑔 ∖ 𝑓 ) = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) )
140 139 rspceeqv ⊢ ( ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∈ 𝑋 ∧ 𝑘 = ∪ dom ( ( 𝑛 ∈ 𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓 ‘ 𝑛 ) ) ) ∖ 𝑓 ) ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) )
141 92 136 140 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) ∧ 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) )
142 141 ex ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
143 142 exlimdv ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ∃ 𝑥 𝑥 ∈ ( ∪ ( 𝐹 ‘ 𝑘 ) ∖ { ( 𝑓 ‘ 𝑘 ) } ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
144 70 143 syld ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
145 144 expimpd ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( ( 𝑘 ∈ 𝐴 ∧ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) → ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
146 23 breq1d ⊢ ( 𝑛 = 𝑘 → ( ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o ↔ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) )
147 146 notbid ⊢ ( 𝑛 = 𝑘 → ( ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o ↔ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) )
148 147 elrab ⊢ ( 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ↔ ( 𝑘 ∈ 𝐴 ∧ ¬ ∪ ( 𝐹 ‘ 𝑘 ) ≈ 1o ) )
149 44 elrnmpt ⊢ ( 𝑘 ∈ V → ( 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ↔ ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
150 149 elv ⊢ ( 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ↔ ∃ 𝑔 ∈ 𝑋 𝑘 = ∪ dom ( 𝑔 ∖ 𝑓 ) )
151 145 148 150 3imtr4g ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } → 𝑘 ∈ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) )
152 151 ssrdv ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) )
153 ssnum ⊢ ( ( ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ∈ dom card ∧ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ ran ( 𝑔 ∈ 𝑋 ↦ ∪ dom ( 𝑔 ∖ 𝑓 ) ) ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card )
154 50 152 153 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card )
155 xpnum ⊢ ( ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card ∧ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ dom card ) → ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card )
156 36 154 155 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card )
157 3 adantr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → 𝐴 ∈ 𝑉 )
158 rabexg ⊢ ( 𝐴 ∈ 𝑉 → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V )
159 157 158 syl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V )
160 fvex ⊢ ( 𝐹 ‘ 𝑘 ) ∈ V
161 160 uniex ⊢ ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
162 161 rgenw ⊢ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V
163 iunexg ⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ∧ ∀ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V )
164 159 162 163 sylancl ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V )
165 resixp ⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ⊆ 𝐴 ∧ 𝑓 ∈ X 𝑘 ∈ 𝐴 ∪ ( 𝐹 ‘ 𝑘 ) ) → ( 𝑓 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) )
166 29 54 165 sylancr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ( 𝑓 ↾ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) )
167 166 ne0d ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ )
168 ixpiunwdom ⊢ ( ( { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∈ V ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ V ∧ X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≠ ∅ ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) )
169 159 164 167 168 syl3anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) )
170 numwdom ⊢ ( ( ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ∈ dom card ∧ ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) × { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ) ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
171 156 169 170 syl2anc ⊢ ( ( 𝜑 ∧ 𝑓 ∈ 𝑋 ) → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )
172 21 171 exlimddv ⊢ ( 𝜑 → ∪ 𝑘 ∈ { 𝑛 ∈ 𝐴 ∣ ¬ ∪ ( 𝐹 ‘ 𝑛 ) ≈ 1o } ∪ ( 𝐹 ‘ 𝑘 ) ∈ dom card )