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 0fin ∅ ∈ 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 𝑘𝐴 ( 𝐹𝑘 ) –ontoX 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
34 29 31 33 sylancr ( ( 𝜑𝑓𝑋 ) → ( 𝑔X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑔 ↾ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ) : X 𝑘𝐴 ( 𝐹𝑘 ) –ontoX 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
35 fonum ( ( X 𝑘𝐴 ( 𝐹𝑘 ) ∈ dom card ∧ ( 𝑔X 𝑘𝐴 ( 𝐹𝑘 ) ↦ ( 𝑔 ↾ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ) : X 𝑘𝐴 ( 𝐹𝑘 ) –ontoX 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 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 syl5bir ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) = ∅ → ( 𝐹𝑘 ) ≈ 1o ) )
68 67 con3d ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( ¬ ( 𝐹𝑘 ) ≈ 1o → ¬ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) = ∅ ) )
69 neq0 ( ¬ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) = ∅ ↔ ∃ 𝑥 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) )
70 68 69 syl6ib ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( ¬ ( 𝐹𝑘 ) ≈ 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 vex 𝑘 ∈ V
94 93 unisn { 𝑘 } = 𝑘
95 simplr ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → 𝑘𝐴 )
96 eleq1w ( 𝑚 = 𝑘 → ( 𝑚𝐴𝑘𝐴 ) )
97 95 96 syl5ibrcom ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ( 𝑚 = 𝑘𝑚𝐴 ) )
98 97 pm4.71rd ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚𝐴𝑚 = 𝑘 ) ) )
99 equequ1 ( 𝑛 = 𝑚 → ( 𝑛 = 𝑘𝑚 = 𝑘 ) )
100 fveq2 ( 𝑛 = 𝑚 → ( 𝑓𝑛 ) = ( 𝑓𝑚 ) )
101 99 100 ifbieq2d ( 𝑛 = 𝑚 → if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) )
102 eqid ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) = ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) )
103 vex 𝑥 ∈ V
104 fvex ( 𝑓𝑚 ) ∈ V
105 103 104 ifex if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ∈ V
106 101 102 105 fvmpt ( 𝑚𝐴 → ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) = if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) )
107 106 neeq1d ( 𝑚𝐴 → ( ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) ) )
108 107 adantl ( ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) ∧ 𝑚𝐴 ) → ( ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ↔ if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) ) )
109 iffalse ( ¬ 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) = ( 𝑓𝑚 ) )
110 109 necon1ai ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) → 𝑚 = 𝑘 )
111 eldifsni ( 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) → 𝑥 ≠ ( 𝑓𝑘 ) )
112 111 ad2antlr ( ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) ∧ 𝑚𝐴 ) → 𝑥 ≠ ( 𝑓𝑘 ) )
113 iftrue ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) = 𝑥 )
114 fveq2 ( 𝑚 = 𝑘 → ( 𝑓𝑚 ) = ( 𝑓𝑘 ) )
115 113 114 neeq12d ( 𝑚 = 𝑘 → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) ↔ 𝑥 ≠ ( 𝑓𝑘 ) ) )
116 112 115 syl5ibrcom ( ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) ∧ 𝑚𝐴 ) → ( 𝑚 = 𝑘 → if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) ) )
117 110 116 impbid2 ( ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) ∧ 𝑚𝐴 ) → ( if ( 𝑚 = 𝑘 , 𝑥 , ( 𝑓𝑚 ) ) ≠ ( 𝑓𝑚 ) ↔ 𝑚 = 𝑘 ) )
118 108 117 bitrd ( ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) ∧ 𝑚𝐴 ) → ( ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ↔ 𝑚 = 𝑘 ) )
119 118 pm5.32da ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ( ( 𝑚𝐴 ∧ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ) ↔ ( 𝑚𝐴𝑚 = 𝑘 ) ) )
120 98 119 bitr4d ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ( 𝑚 = 𝑘 ↔ ( 𝑚𝐴 ∧ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ) ) )
121 120 abbidv ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → { 𝑚𝑚 = 𝑘 } = { 𝑚 ∣ ( 𝑚𝐴 ∧ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ) } )
122 df-sn { 𝑘 } = { 𝑚𝑚 = 𝑘 }
123 df-rab { 𝑚𝐴 ∣ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) } = { 𝑚 ∣ ( 𝑚𝐴 ∧ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) ) }
124 121 122 123 3eqtr4g ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → { 𝑘 } = { 𝑚𝐴 ∣ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) } )
125 fvex ( 𝑓𝑛 ) ∈ V
126 103 125 ifex if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ∈ V
127 126 rgenw 𝑛𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ∈ V
128 102 fnmpt ( ∀ 𝑛𝐴 if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ∈ V → ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) Fn 𝐴 )
129 127 128 mp1i ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) Fn 𝐴 )
130 ixpfn ( 𝑓X 𝑛𝐴 ( 𝐹𝑛 ) → 𝑓 Fn 𝐴 )
131 76 130 syl ( ( 𝜑𝑓𝑋 ) → 𝑓 Fn 𝐴 )
132 131 ad2antrr ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → 𝑓 Fn 𝐴 )
133 fndmdif ( ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) Fn 𝐴𝑓 Fn 𝐴 ) → dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚𝐴 ∣ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) } )
134 129 132 133 syl2anc ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) = { 𝑚𝐴 ∣ ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ‘ 𝑚 ) ≠ ( 𝑓𝑚 ) } )
135 124 134 eqtr4d ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → { 𝑘 } = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
136 135 unieqd ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → { 𝑘 } = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
137 94 136 eqtr3id ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → 𝑘 = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
138 difeq1 ( 𝑔 = ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) → ( 𝑔𝑓 ) = ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
139 138 dmeqd ( 𝑔 = ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) → dom ( 𝑔𝑓 ) = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
140 139 unieqd ( 𝑔 = ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) → dom ( 𝑔𝑓 ) = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) )
141 140 rspceeqv ( ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∈ 𝑋𝑘 = dom ( ( 𝑛𝐴 ↦ if ( 𝑛 = 𝑘 , 𝑥 , ( 𝑓𝑛 ) ) ) ∖ 𝑓 ) ) → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) )
142 92 137 141 syl2anc ( ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) ∧ 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) ) → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) )
143 142 ex ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) ) )
144 143 exlimdv ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( ∃ 𝑥 𝑥 ∈ ( ( 𝐹𝑘 ) ∖ { ( 𝑓𝑘 ) } ) → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) ) )
145 70 144 syld ( ( ( 𝜑𝑓𝑋 ) ∧ 𝑘𝐴 ) → ( ¬ ( 𝐹𝑘 ) ≈ 1o → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) ) )
146 145 expimpd ( ( 𝜑𝑓𝑋 ) → ( ( 𝑘𝐴 ∧ ¬ ( 𝐹𝑘 ) ≈ 1o ) → ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) ) )
147 23 breq1d ( 𝑛 = 𝑘 → ( ( 𝐹𝑛 ) ≈ 1o ( 𝐹𝑘 ) ≈ 1o ) )
148 147 notbid ( 𝑛 = 𝑘 → ( ¬ ( 𝐹𝑛 ) ≈ 1o ↔ ¬ ( 𝐹𝑘 ) ≈ 1o ) )
149 148 elrab ( 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ↔ ( 𝑘𝐴 ∧ ¬ ( 𝐹𝑘 ) ≈ 1o ) )
150 44 elrnmpt ( 𝑘 ∈ V → ( 𝑘 ∈ ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) ↔ ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) ) )
151 150 elv ( 𝑘 ∈ ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) ↔ ∃ 𝑔𝑋 𝑘 = dom ( 𝑔𝑓 ) )
152 146 149 151 3imtr4g ( ( 𝜑𝑓𝑋 ) → ( 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } → 𝑘 ∈ ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) ) )
153 152 ssrdv ( ( 𝜑𝑓𝑋 ) → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⊆ ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) )
154 ssnum ( ( ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) ∈ dom card ∧ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⊆ ran ( 𝑔𝑋 dom ( 𝑔𝑓 ) ) ) → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ dom card )
155 50 153 154 syl2anc ( ( 𝜑𝑓𝑋 ) → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ dom card )
156 xpnum ( ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card ∧ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ dom card ) → ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ∈ dom card )
157 36 155 156 syl2anc ( ( 𝜑𝑓𝑋 ) → ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ∈ dom card )
158 3 adantr ( ( 𝜑𝑓𝑋 ) → 𝐴𝑉 )
159 rabexg ( 𝐴𝑉 → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V )
160 158 159 syl ( ( 𝜑𝑓𝑋 ) → { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V )
161 fvex ( 𝐹𝑘 ) ∈ V
162 161 uniex ( 𝐹𝑘 ) ∈ V
163 162 rgenw 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ V
164 iunexg ( ( { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V ∧ ∀ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ V ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ V )
165 160 163 164 sylancl ( ( 𝜑𝑓𝑋 ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ V )
166 resixp ( ( { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ⊆ 𝐴𝑓X 𝑘𝐴 ( 𝐹𝑘 ) ) → ( 𝑓 ↾ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
167 29 54 166 sylancr ( ( 𝜑𝑓𝑋 ) → ( 𝑓 ↾ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ∈ X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) )
168 167 ne0d ( ( 𝜑𝑓𝑋 ) → X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ≠ ∅ )
169 ixpiunwdom ( ( { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ∈ V ∧ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ V ∧ X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ≠ ∅ ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) )
170 160 165 168 169 syl3anc ( ( 𝜑𝑓𝑋 ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) )
171 numwdom ( ( ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ∈ dom card ∧ 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ≼* ( X 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) × { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ) ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card )
172 157 170 171 syl2anc ( ( 𝜑𝑓𝑋 ) → 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card )
173 21 172 exlimddv ( 𝜑 𝑘 ∈ { 𝑛𝐴 ∣ ¬ ( 𝐹𝑛 ) ≈ 1o } ( 𝐹𝑘 ) ∈ dom card )