Metamath Proof Explorer

Theorem ramub1lem1

Description: Lemma for ramub1 . (Contributed by Mario Carneiro, 23-Apr-2015)

Ref Expression
Hypotheses ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
ramub1.3 ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
ramub1.4 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
ramub1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
ramub1.6 ⊢ ( 𝜑 → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
ramub1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
ramub1.h ⊢ 𝐻 = ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↦ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) )
ramub1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑅 )
ramub1.w ⊢ ( 𝜑 → 𝑊 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
ramub1.7 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) ≤ ( ♯ ‘ 𝑊 ) )
ramub1.8 ⊢ ( 𝜑 → ( 𝑊 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝐷 } ) )
ramub1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑅 )
ramub1.v ⊢ ( 𝜑 → 𝑉 ⊆ 𝑊 )
ramub1.9 ⊢ ( 𝜑 → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) ≤ ( ♯ ‘ 𝑉 ) )
ramub1.s ⊢ ( 𝜑 → ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
Assertion ramub1lem1 ( 𝜑 → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ )
2 ramub1.r ⊢ ( 𝜑 → 𝑅 ∈ Fin )
3 ramub1.f ⊢ ( 𝜑 → 𝐹 : 𝑅 ⟶ ℕ )
4 ramub1.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑅 ↦ ( 𝑀 Ramsey ( 𝑦 ∈ 𝑅 ↦ if ( 𝑦 = 𝑥 , ( ( 𝐹 ‘ 𝑥 ) − 1 ) , ( 𝐹 ‘ 𝑦 ) ) ) ) )
5 ramub1.1 ⊢ ( 𝜑 → 𝐺 : 𝑅 ⟶ ℕ0 )
6 ramub1.2 ⊢ ( 𝜑 → ( ( 𝑀 − 1 ) Ramsey 𝐺 ) ∈ ℕ0 )
7 ramub1.3 ⊢ 𝐶 = ( 𝑎 ∈ V , 𝑖 ∈ ℕ0 ↦ { 𝑏 ∈ 𝒫 𝑎 ∣ ( ♯ ‘ 𝑏 ) = 𝑖 } )
8 ramub1.4 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
9 ramub1.5 ⊢ ( 𝜑 → ( ♯ ‘ 𝑆 ) = ( ( ( 𝑀 − 1 ) Ramsey 𝐺 ) + 1 ) )
10 ramub1.6 ⊢ ( 𝜑 → 𝐾 : ( 𝑆 𝐶 𝑀 ) ⟶ 𝑅 )
11 ramub1.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
12 ramub1.h ⊢ 𝐻 = ( 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ↦ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) )
13 ramub1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑅 )
14 ramub1.w ⊢ ( 𝜑 → 𝑊 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
15 ramub1.7 ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐷 ) ≤ ( ♯ ‘ 𝑊 ) )
16 ramub1.8 ⊢ ( 𝜑 → ( 𝑊 𝐶 ( 𝑀 − 1 ) ) ⊆ ( ◡ 𝐻 “ { 𝐷 } ) )
17 ramub1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑅 )
18 ramub1.v ⊢ ( 𝜑 → 𝑉 ⊆ 𝑊 )
19 ramub1.9 ⊢ ( 𝜑 → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) ≤ ( ♯ ‘ 𝑉 ) )
20 ramub1.s ⊢ ( 𝜑 → ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
21 18 14 sstrd ⊢ ( 𝜑 → 𝑉 ⊆ ( 𝑆 ∖ { 𝑋 } ) )
22 21 difss2d ⊢ ( 𝜑 → 𝑉 ⊆ 𝑆 )
23 11 snssd ⊢ ( 𝜑 → { 𝑋 } ⊆ 𝑆 )
24 22 23 unssd ⊢ ( 𝜑 → ( 𝑉 ∪ { 𝑋 } ) ⊆ 𝑆 )
25 8 24 sselpwd ⊢ ( 𝜑 → ( 𝑉 ∪ { 𝑋 } ) ∈ 𝒫 𝑆 )
26 25 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( 𝑉 ∪ { 𝑋 } ) ∈ 𝒫 𝑆 )
27 iftrue ⊢ ( 𝐸 = 𝐷 → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) = ( ( 𝐹 ‘ 𝐷 ) − 1 ) )
28 27 adantl ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) = ( ( 𝐹 ‘ 𝐷 ) − 1 ) )
29 19 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) ≤ ( ♯ ‘ 𝑉 ) )
30 28 29 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ( 𝐹 ‘ 𝐷 ) − 1 ) ≤ ( ♯ ‘ 𝑉 ) )
31 3 13 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐷 ) ∈ ℕ )
32 31 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( 𝐹 ‘ 𝐷 ) ∈ ℕ )
33 32 nnred ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( 𝐹 ‘ 𝐷 ) ∈ ℝ )
34 1red ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → 1 ∈ ℝ )
35 8 22 ssfid ⊢ ( 𝜑 → 𝑉 ∈ Fin )
36 hashcl ⊢ ( 𝑉 ∈ Fin → ( ♯ ‘ 𝑉 ) ∈ ℕ0 )
37 nn0re ⊢ ( ( ♯ ‘ 𝑉 ) ∈ ℕ0 → ( ♯ ‘ 𝑉 ) ∈ ℝ )
38 35 36 37 3syl ⊢ ( 𝜑 → ( ♯ ‘ 𝑉 ) ∈ ℝ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ♯ ‘ 𝑉 ) ∈ ℝ )
40 33 34 39 lesubaddd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ( ( 𝐹 ‘ 𝐷 ) − 1 ) ≤ ( ♯ ‘ 𝑉 ) ↔ ( 𝐹 ‘ 𝐷 ) ≤ ( ( ♯ ‘ 𝑉 ) + 1 ) ) )
41 30 40 mpbid ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( 𝐹 ‘ 𝐷 ) ≤ ( ( ♯ ‘ 𝑉 ) + 1 ) )
42 fveq2 ⊢ ( 𝐸 = 𝐷 → ( 𝐹 ‘ 𝐸 ) = ( 𝐹 ‘ 𝐷 ) )
43 snidg ⊢ ( 𝑋 ∈ 𝑆 → 𝑋 ∈ { 𝑋 } )
44 11 43 syl ⊢ ( 𝜑 → 𝑋 ∈ { 𝑋 } )
45 21 sseld ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑉 → 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) ) )
46 eldifn ⊢ ( 𝑋 ∈ ( 𝑆 ∖ { 𝑋 } ) → ¬ 𝑋 ∈ { 𝑋 } )
47 45 46 syl6 ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑉 → ¬ 𝑋 ∈ { 𝑋 } ) )
48 44 47 mt2d ⊢ ( 𝜑 → ¬ 𝑋 ∈ 𝑉 )
49 hashunsng ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝑉 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑉 ) + 1 ) ) )
50 11 49 syl ⊢ ( 𝜑 → ( ( 𝑉 ∈ Fin ∧ ¬ 𝑋 ∈ 𝑉 ) → ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑉 ) + 1 ) ) )
51 35 48 50 mp2and ⊢ ( 𝜑 → ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) = ( ( ♯ ‘ 𝑉 ) + 1 ) )
52 42 51 breqan12rd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) ↔ ( 𝐹 ‘ 𝐷 ) ≤ ( ( ♯ ‘ 𝑉 ) + 1 ) ) )
53 41 52 mpbird ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) )
54 snfi ⊢ { 𝑋 } ∈ Fin
55 unfi ⊢ ( ( 𝑉 ∈ Fin ∧ { 𝑋 } ∈ Fin ) → ( 𝑉 ∪ { 𝑋 } ) ∈ Fin )
56 35 54 55 sylancl ⊢ ( 𝜑 → ( 𝑉 ∪ { 𝑋 } ) ∈ Fin )
57 1 nnnn0d ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
58 7 hashbcval ⊢ ( ( ( 𝑉 ∪ { 𝑋 } ) ∈ Fin ∧ 𝑀 ∈ ℕ0 ) → ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
59 56 57 58 syl2anc ⊢ ( 𝜑 → ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
61 simpl1l ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → 𝜑 )
62 7 hashbcval ⊢ ( ( 𝑉 ∈ Fin ∧ 𝑀 ∈ ℕ0 ) → ( 𝑉 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
63 35 57 62 syl2anc ⊢ ( 𝜑 → ( 𝑉 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
64 63 20 eqsstrrd ⊢ ( 𝜑 → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
65 61 64 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
66 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ 𝒫 𝑉 )
67 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ 𝑥 ) = 𝑀 )
68 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } ↔ ( 𝑥 ∈ 𝒫 𝑉 ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) )
69 66 67 68 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ { 𝑥 ∈ 𝒫 𝑉 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
70 65 69 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ ( ◡ 𝐾 “ { 𝐸 } ) )
71 simpl2 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) )
72 71 elpwid ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ⊆ ( 𝑉 ∪ { 𝑋 } ) )
73 simpl1l ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝜑 )
74 73 24 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑉 ∪ { 𝑋 } ) ⊆ 𝑆 )
75 72 74 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ⊆ 𝑆 )
76 vex ⊢ 𝑥 ∈ V
77 76 elpw ⊢ ( 𝑥 ∈ 𝒫 𝑆 ↔ 𝑥 ⊆ 𝑆 )
78 75 77 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ 𝒫 𝑆 )
79 simpl3 ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ 𝑥 ) = 𝑀 )
80 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } ↔ ( 𝑥 ∈ 𝒫 𝑆 ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) )
81 78 79 80 sylanbrc ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
82 7 hashbcval ⊢ ( ( 𝑆 ∈ Fin ∧ 𝑀 ∈ ℕ0 ) → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
83 8 57 82 syl2anc ⊢ ( 𝜑 → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
84 73 83 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑆 𝐶 𝑀 ) = { 𝑥 ∈ 𝒫 𝑆 ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } )
85 81 84 eleqtrrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ ( 𝑆 𝐶 𝑀 ) )
86 14 difss2d ⊢ ( 𝜑 → 𝑊 ⊆ 𝑆 )
87 8 86 ssfid ⊢ ( 𝜑 → 𝑊 ∈ Fin )
88 nnm1nn0 ⊢ ( 𝑀 ∈ ℕ → ( 𝑀 − 1 ) ∈ ℕ0 )
89 1 88 syl ⊢ ( 𝜑 → ( 𝑀 − 1 ) ∈ ℕ0 )
90 7 hashbcval ⊢ ( ( 𝑊 ∈ Fin ∧ ( 𝑀 − 1 ) ∈ ℕ0 ) → ( 𝑊 𝐶 ( 𝑀 − 1 ) ) = { 𝑢 ∈ 𝒫 𝑊 ∣ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) } )
91 87 89 90 syl2anc ⊢ ( 𝜑 → ( 𝑊 𝐶 ( 𝑀 − 1 ) ) = { 𝑢 ∈ 𝒫 𝑊 ∣ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) } )
92 91 16 eqsstrrd ⊢ ( 𝜑 → { 𝑢 ∈ 𝒫 𝑊 ∣ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) } ⊆ ( ◡ 𝐻 “ { 𝐷 } ) )
93 73 92 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → { 𝑢 ∈ 𝒫 𝑊 ∣ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) } ⊆ ( ◡ 𝐻 “ { 𝐷 } ) )
94 fveqeq2 ⊢ ( 𝑢 = ( 𝑥 ∖ { 𝑋 } ) → ( ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) ↔ ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) = ( 𝑀 − 1 ) ) )
95 uncom ⊢ ( 𝑉 ∪ { 𝑋 } ) = ( { 𝑋 } ∪ 𝑉 )
96 72 95 sseqtrdi ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ⊆ ( { 𝑋 } ∪ 𝑉 ) )
97 ssundif ⊢ ( 𝑥 ⊆ ( { 𝑋 } ∪ 𝑉 ) ↔ ( 𝑥 ∖ { 𝑋 } ) ⊆ 𝑉 )
98 96 97 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ⊆ 𝑉 )
99 73 18 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑉 ⊆ 𝑊 )
100 98 99 sstrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ⊆ 𝑊 )
101 76 difexi ⊢ ( 𝑥 ∖ { 𝑋 } ) ∈ V
102 101 elpw ⊢ ( ( 𝑥 ∖ { 𝑋 } ) ∈ 𝒫 𝑊 ↔ ( 𝑥 ∖ { 𝑋 } ) ⊆ 𝑊 )
103 100 102 sylibr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ∈ 𝒫 𝑊 )
104 73 8 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑆 ∈ Fin )
105 104 75 ssfid ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ Fin )
106 diffi ⊢ ( 𝑥 ∈ Fin → ( 𝑥 ∖ { 𝑋 } ) ∈ Fin )
107 105 106 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ∈ Fin )
108 hashcl ⊢ ( ( 𝑥 ∖ { 𝑋 } ) ∈ Fin → ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) ∈ ℕ0 )
109 nn0cn ⊢ ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) ∈ ℕ0 → ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) ∈ ℂ )
110 107 108 109 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) ∈ ℂ )
111 ax-1cn ⊢ 1 ∈ ℂ
112 pncan ⊢ ( ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) − 1 ) = ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) )
113 110 111 112 sylancl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) − 1 ) = ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) )
114 neldifsnd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ¬ 𝑋 ∈ ( 𝑥 ∖ { 𝑋 } ) )
115 hashunsng ⊢ ( 𝑋 ∈ 𝑆 → ( ( ( 𝑥 ∖ { 𝑋 } ) ∈ Fin ∧ ¬ 𝑋 ∈ ( 𝑥 ∖ { 𝑋 } ) ) → ( ♯ ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) ) )
116 73 11 115 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ( ( 𝑥 ∖ { 𝑋 } ) ∈ Fin ∧ ¬ 𝑋 ∈ ( 𝑥 ∖ { 𝑋 } ) ) → ( ♯ ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) ) )
117 107 114 116 mp2and ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) )
118 undif1 ⊢ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) = ( 𝑥 ∪ { 𝑋 } )
119 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ¬ 𝑥 ∈ 𝒫 𝑉 )
120 71 119 eldifd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ ( 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∖ 𝒫 𝑉 ) )
121 elpwunsn ⊢ ( 𝑥 ∈ ( 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∖ 𝒫 𝑉 ) → 𝑋 ∈ 𝑥 )
122 120 121 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑋 ∈ 𝑥 )
123 122 snssd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → { 𝑋 } ⊆ 𝑥 )
124 ssequn2 ⊢ ( { 𝑋 } ⊆ 𝑥 ↔ ( 𝑥 ∪ { 𝑋 } ) = 𝑥 )
125 123 124 sylib ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∪ { 𝑋 } ) = 𝑥 )
126 118 125 eqtr2id ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 = ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) )
127 126 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) )
128 127 79 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = 𝑀 )
129 117 128 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) = 𝑀 )
130 129 oveq1d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ( ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) + 1 ) − 1 ) = ( 𝑀 − 1 ) )
131 113 130 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ♯ ‘ ( 𝑥 ∖ { 𝑋 } ) ) = ( 𝑀 − 1 ) )
132 94 103 131 elrabd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ∈ { 𝑢 ∈ 𝒫 𝑊 ∣ ( ♯ ‘ 𝑢 ) = ( 𝑀 − 1 ) } )
133 93 132 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ∈ ( ◡ 𝐻 “ { 𝐷 } ) )
134 12 mptiniseg ⊢ ( 𝐷 ∈ 𝑅 → ( ◡ 𝐻 “ { 𝐷 } ) = { 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∣ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 } )
135 73 13 134 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( ◡ 𝐻 “ { 𝐷 } ) = { 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∣ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 } )
136 133 135 eleqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∖ { 𝑋 } ) ∈ { 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∣ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 } )
137 uneq1 ⊢ ( 𝑢 = ( 𝑥 ∖ { 𝑋 } ) → ( 𝑢 ∪ { 𝑋 } ) = ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) )
138 137 fveqeq2d ⊢ ( 𝑢 = ( 𝑥 ∖ { 𝑋 } ) → ( ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 ↔ ( 𝐾 ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = 𝐷 ) )
139 138 elrab ⊢ ( ( 𝑥 ∖ { 𝑋 } ) ∈ { 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∣ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 } ↔ ( ( 𝑥 ∖ { 𝑋 } ) ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∧ ( 𝐾 ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = 𝐷 ) )
140 139 simprbi ⊢ ( ( 𝑥 ∖ { 𝑋 } ) ∈ { 𝑢 ∈ ( ( 𝑆 ∖ { 𝑋 } ) 𝐶 ( 𝑀 − 1 ) ) ∣ ( 𝐾 ‘ ( 𝑢 ∪ { 𝑋 } ) ) = 𝐷 } → ( 𝐾 ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = 𝐷 )
141 136 140 syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝐾 ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) = 𝐷 )
142 126 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ ( ( 𝑥 ∖ { 𝑋 } ) ∪ { 𝑋 } ) ) )
143 simpl1r ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝐸 = 𝐷 )
144 141 142 143 3eqtr4d ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝐾 ‘ 𝑥 ) = 𝐸 )
145 10 ffnd ⊢ ( 𝜑 → 𝐾 Fn ( 𝑆 𝐶 𝑀 ) )
146 fniniseg ⊢ ( 𝐾 Fn ( 𝑆 𝐶 𝑀 ) → ( 𝑥 ∈ ( ◡ 𝐾 “ { 𝐸 } ) ↔ ( 𝑥 ∈ ( 𝑆 𝐶 𝑀 ) ∧ ( 𝐾 ‘ 𝑥 ) = 𝐸 ) ) )
147 73 145 146 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → ( 𝑥 ∈ ( ◡ 𝐾 “ { 𝐸 } ) ↔ ( 𝑥 ∈ ( 𝑆 𝐶 𝑀 ) ∧ ( 𝐾 ‘ 𝑥 ) = 𝐸 ) ) )
148 85 144 147 mpbir2and ⊢ ( ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) ∧ ¬ 𝑥 ∈ 𝒫 𝑉 ) → 𝑥 ∈ ( ◡ 𝐾 “ { 𝐸 } ) )
149 70 148 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝐸 = 𝐷 ) ∧ 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∧ ( ♯ ‘ 𝑥 ) = 𝑀 ) → 𝑥 ∈ ( ◡ 𝐾 “ { 𝐸 } ) )
150 149 rabssdv ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → { 𝑥 ∈ 𝒫 ( 𝑉 ∪ { 𝑋 } ) ∣ ( ♯ ‘ 𝑥 ) = 𝑀 } ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
151 60 150 eqsstrd ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
152 fveq2 ⊢ ( 𝑧 = ( 𝑉 ∪ { 𝑋 } ) → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) )
153 152 breq2d ⊢ ( 𝑧 = ( 𝑉 ∪ { 𝑋 } ) → ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) ) )
154 oveq1 ⊢ ( 𝑧 = ( 𝑉 ∪ { 𝑋 } ) → ( 𝑧 𝐶 𝑀 ) = ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) )
155 154 sseq1d ⊢ ( 𝑧 = ( 𝑉 ∪ { 𝑋 } ) → ( ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ↔ ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
156 153 155 anbi12d ⊢ ( 𝑧 = ( 𝑉 ∪ { 𝑋 } ) → ( ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ↔ ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) ∧ ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ) )
157 156 rspcev ⊢ ( ( ( 𝑉 ∪ { 𝑋 } ) ∈ 𝒫 𝑆 ∧ ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ ( 𝑉 ∪ { 𝑋 } ) ) ∧ ( ( 𝑉 ∪ { 𝑋 } ) 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
158 26 53 151 157 syl12anc ⊢ ( ( 𝜑 ∧ 𝐸 = 𝐷 ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
159 8 22 sselpwd ⊢ ( 𝜑 → 𝑉 ∈ 𝒫 𝑆 )
160 159 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → 𝑉 ∈ 𝒫 𝑆 )
161 ifnefalse ⊢ ( 𝐸 ≠ 𝐷 → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) )
162 161 adantl ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) = ( 𝐹 ‘ 𝐸 ) )
163 19 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → if ( 𝐸 = 𝐷 , ( ( 𝐹 ‘ 𝐷 ) − 1 ) , ( 𝐹 ‘ 𝐸 ) ) ≤ ( ♯ ‘ 𝑉 ) )
164 162 163 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑉 ) )
165 20 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) )
166 fveq2 ⊢ ( 𝑧 = 𝑉 → ( ♯ ‘ 𝑧 ) = ( ♯ ‘ 𝑉 ) )
167 166 breq2d ⊢ ( 𝑧 = 𝑉 → ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑉 ) ) )
168 oveq1 ⊢ ( 𝑧 = 𝑉 → ( 𝑧 𝐶 𝑀 ) = ( 𝑉 𝐶 𝑀 ) )
169 168 sseq1d ⊢ ( 𝑧 = 𝑉 → ( ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ↔ ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
170 167 169 anbi12d ⊢ ( 𝑧 = 𝑉 → ( ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ↔ ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑉 ) ∧ ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ) )
171 170 rspcev ⊢ ( ( 𝑉 ∈ 𝒫 𝑆 ∧ ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑉 ) ∧ ( 𝑉 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
172 160 164 165 171 syl12anc ⊢ ( ( 𝜑 ∧ 𝐸 ≠ 𝐷 ) → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )
173 158 172 pm2.61dane ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝒫 𝑆 ( ( 𝐹 ‘ 𝐸 ) ≤ ( ♯ ‘ 𝑧 ) ∧ ( 𝑧 𝐶 𝑀 ) ⊆ ( ◡ 𝐾 “ { 𝐸 } ) ) )