Metamath Proof Explorer

Theorem ramub1lem2

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

Ref Expression
Hypotheses ramub1.m ⊢ φ → M ∈ ℕ
ramub1.r ⊢ φ → R ∈ Fin
ramub1.f ⊢ φ → F : R ⟶ ℕ
ramub1.g ⊢ G = x ∈ R ⟼ M Ramsey y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y
ramub1.1 ⊢ φ → G : R ⟶ ℕ 0
ramub1.2 ⊢ φ → M − 1 Ramsey G ∈ ℕ 0
ramub1.3 ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
ramub1.4 ⊢ φ → S ∈ Fin
ramub1.5 ⊢ φ → S = M − 1 Ramsey G + 1
ramub1.6 ⊢ φ → K : S C M ⟶ R
ramub1.x ⊢ φ → X ∈ S
ramub1.h ⊢ H = u ∈ S ∖ X C M − 1 ⟼ K ⁡ u ∪ X
Assertion ramub1lem2 ⊢ φ → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c

Proof

Step Hyp Ref Expression
1 ramub1.m ⊢ φ → M ∈ ℕ
2 ramub1.r ⊢ φ → R ∈ Fin
3 ramub1.f ⊢ φ → F : R ⟶ ℕ
4 ramub1.g ⊢ G = x ∈ R ⟼ M Ramsey y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y
5 ramub1.1 ⊢ φ → G : R ⟶ ℕ 0
6 ramub1.2 ⊢ φ → M − 1 Ramsey G ∈ ℕ 0
7 ramub1.3 ⊢ C = a ∈ V , i ∈ ℕ 0 ⟼ b ∈ 𝒫 a | b = i
8 ramub1.4 ⊢ φ → S ∈ Fin
9 ramub1.5 ⊢ φ → S = M − 1 Ramsey G + 1
10 ramub1.6 ⊢ φ → K : S C M ⟶ R
11 ramub1.x ⊢ φ → X ∈ S
12 ramub1.h ⊢ H = u ∈ S ∖ X C M − 1 ⟼ K ⁡ u ∪ X
13 nnm1nn0 ⊢ M ∈ ℕ → M − 1 ∈ ℕ 0
14 1 13 syl ⊢ φ → M − 1 ∈ ℕ 0
15 diffi ⊢ S ∈ Fin → S ∖ X ∈ Fin
16 8 15 syl ⊢ φ → S ∖ X ∈ Fin
17 6 nn0red ⊢ φ → M − 1 Ramsey G ∈ ℝ
18 17 leidd ⊢ φ → M − 1 Ramsey G ≤ M − 1 Ramsey G
19 hashcl ⊢ S ∖ X ∈ Fin → S ∖ X ∈ ℕ 0
20 16 19 syl ⊢ φ → S ∖ X ∈ ℕ 0
21 20 nn0cnd ⊢ φ → S ∖ X ∈ ℂ
22 6 nn0cnd ⊢ φ → M − 1 Ramsey G ∈ ℂ
23 1cnd ⊢ φ → 1 ∈ ℂ
24 undif1 ⊢ S ∖ X ∪ X = S ∪ X
25 11 snssd ⊢ φ → X ⊆ S
26 ssequn2 ⊢ X ⊆ S ↔ S ∪ X = S
27 25 26 sylib ⊢ φ → S ∪ X = S
28 24 27 eqtrid ⊢ φ → S ∖ X ∪ X = S
29 28 fveq2d ⊢ φ → S ∖ X ∪ X = S
30 neldifsnd ⊢ φ → ¬ X ∈ S ∖ X
31 hashunsng ⊢ X ∈ S → S ∖ X ∈ Fin ∧ ¬ X ∈ S ∖ X → S ∖ X ∪ X = S ∖ X + 1
32 11 31 syl ⊢ φ → S ∖ X ∈ Fin ∧ ¬ X ∈ S ∖ X → S ∖ X ∪ X = S ∖ X + 1
33 16 30 32 mp2and ⊢ φ → S ∖ X ∪ X = S ∖ X + 1
34 29 33 9 3eqtr3d ⊢ φ → S ∖ X + 1 = M − 1 Ramsey G + 1
35 21 22 23 34 addcan2ad ⊢ φ → S ∖ X = M − 1 Ramsey G
36 18 35 breqtrrd ⊢ φ → M − 1 Ramsey G ≤ S ∖ X
37 10 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → K : S C M ⟶ R
38 fveqeq2 ⊢ x = u ∪ X → x = M ↔ u ∪ X = M
39 7 hashbcval ⊢ S ∖ X ∈ Fin ∧ M − 1 ∈ ℕ 0 → S ∖ X C M − 1 = x ∈ 𝒫 S ∖ X | x = M − 1
40 16 14 39 syl2anc ⊢ φ → S ∖ X C M − 1 = x ∈ 𝒫 S ∖ X | x = M − 1
41 40 eleq2d ⊢ φ → u ∈ S ∖ X C M − 1 ↔ u ∈ x ∈ 𝒫 S ∖ X | x = M − 1
42 fveqeq2 ⊢ x = u → x = M − 1 ↔ u = M − 1
43 42 elrab ⊢ u ∈ x ∈ 𝒫 S ∖ X | x = M − 1 ↔ u ∈ 𝒫 S ∖ X ∧ u = M − 1
44 41 43 bitrdi ⊢ φ → u ∈ S ∖ X C M − 1 ↔ u ∈ 𝒫 S ∖ X ∧ u = M − 1
45 44 simprbda ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∈ 𝒫 S ∖ X
46 45 elpwid ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ⊆ S ∖ X
47 46 difss2d ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ⊆ S
48 25 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → X ⊆ S
49 47 48 unssd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X ⊆ S
50 vex ⊢ u ∈ V
51 snex ⊢ X ∈ V
52 50 51 unex ⊢ u ∪ X ∈ V
53 52 elpw ⊢ u ∪ X ∈ 𝒫 S ↔ u ∪ X ⊆ S
54 49 53 sylibr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X ∈ 𝒫 S
55 16 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → S ∖ X ∈ Fin
56 55 46 ssfid ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∈ Fin
57 neldifsnd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → ¬ X ∈ S ∖ X
58 46 57 ssneldd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → ¬ X ∈ u
59 11 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → X ∈ S
60 hashunsng ⊢ X ∈ S → u ∈ Fin ∧ ¬ X ∈ u → u ∪ X = u + 1
61 59 60 syl ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∈ Fin ∧ ¬ X ∈ u → u ∪ X = u + 1
62 56 58 61 mp2and ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X = u + 1
63 44 simplbda ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u = M − 1
64 63 oveq1d ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u + 1 = M - 1 + 1
65 1 nncnd ⊢ φ → M ∈ ℂ
66 ax-1cn ⊢ 1 ∈ ℂ
67 npcan ⊢ M ∈ ℂ ∧ 1 ∈ ℂ → M - 1 + 1 = M
68 65 66 67 sylancl ⊢ φ → M - 1 + 1 = M
69 68 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → M - 1 + 1 = M
70 62 64 69 3eqtrd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X = M
71 38 54 70 elrabd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X ∈ x ∈ 𝒫 S | x = M
72 1 nnnn0d ⊢ φ → M ∈ ℕ 0
73 7 hashbcval ⊢ S ∈ Fin ∧ M ∈ ℕ 0 → S C M = x ∈ 𝒫 S | x = M
74 8 72 73 syl2anc ⊢ φ → S C M = x ∈ 𝒫 S | x = M
75 74 adantr ⊢ φ ∧ u ∈ S ∖ X C M − 1 → S C M = x ∈ 𝒫 S | x = M
76 71 75 eleqtrrd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → u ∪ X ∈ S C M
77 37 76 ffvelrnd ⊢ φ ∧ u ∈ S ∖ X C M − 1 → K ⁡ u ∪ X ∈ R
78 77 12 fmptd ⊢ φ → H : S ∖ X C M − 1 ⟶ R
79 7 14 2 5 6 16 36 78 rami ⊢ φ → ∃ d ∈ R ∃ w ∈ 𝒫 S ∖ X G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d
80 72 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → M ∈ ℕ 0
81 2 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → R ∈ Fin
82 3 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → F : R ⟶ ℕ
83 simprll ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → d ∈ R
84 82 83 ffvelrnd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → F ⁡ d ∈ ℕ
85 nnm1nn0 ⊢ F ⁡ d ∈ ℕ → F ⁡ d − 1 ∈ ℕ 0
86 84 85 syl ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → F ⁡ d − 1 ∈ ℕ 0
87 86 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ y ∈ R → F ⁡ d − 1 ∈ ℕ 0
88 82 ffvelrnda ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ y ∈ R → F ⁡ y ∈ ℕ
89 88 nnnn0d ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ y ∈ R → F ⁡ y ∈ ℕ 0
90 87 89 ifcld ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ y ∈ R → if y = d F ⁡ d − 1 F ⁡ y ∈ ℕ 0
91 eqid ⊢ y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y = y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y
92 90 91 fmptd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y : R ⟶ ℕ 0
93 equequ2 ⊢ x = d → y = x ↔ y = d
94 fveq2 ⊢ x = d → F ⁡ x = F ⁡ d
95 94 oveq1d ⊢ x = d → F ⁡ x − 1 = F ⁡ d − 1
96 93 95 ifbieq1d ⊢ x = d → if y = x F ⁡ x − 1 F ⁡ y = if y = d F ⁡ d − 1 F ⁡ y
97 96 mpteq2dv ⊢ x = d → y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y = y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y
98 97 oveq2d ⊢ x = d → M Ramsey y ∈ R ⟼ if y = x F ⁡ x − 1 F ⁡ y = M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y
99 ovex ⊢ M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ∈ V
100 98 4 99 fvmpt ⊢ d ∈ R → G ⁡ d = M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y
101 83 100 syl ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → G ⁡ d = M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y
102 5 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → G : R ⟶ ℕ 0
103 102 83 ffvelrnd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → G ⁡ d ∈ ℕ 0
104 101 103 eqeltrrd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ∈ ℕ 0
105 simprlr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → w ∈ 𝒫 S ∖ X
106 simprrl ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → G ⁡ d ≤ w
107 101 106 eqbrtrrd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → M Ramsey y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ≤ w
108 10 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → K : S C M ⟶ R
109 8 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → S ∈ Fin
110 105 elpwid ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → w ⊆ S ∖ X
111 110 difss2d ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → w ⊆ S
112 7 hashbcss ⊢ S ∈ Fin ∧ w ⊆ S ∧ M ∈ ℕ 0 → w C M ⊆ S C M
113 109 111 80 112 syl3anc ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → w C M ⊆ S C M
114 108 113 fssresd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → K ↾ w C M : w C M ⟶ R
115 7 80 81 92 104 105 107 114 rami ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → ∃ c ∈ R ∃ v ∈ 𝒫 w y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c
116 equequ1 ⊢ y = c → y = d ↔ c = d
117 fveq2 ⊢ y = c → F ⁡ y = F ⁡ c
118 116 117 ifbieq2d ⊢ y = c → if y = d F ⁡ d − 1 F ⁡ y = if c = d F ⁡ d − 1 F ⁡ c
119 ovex ⊢ F ⁡ d − 1 ∈ V
120 fvex ⊢ F ⁡ c ∈ V
121 119 120 ifex ⊢ if c = d F ⁡ d − 1 F ⁡ c ∈ V
122 118 91 121 fvmpt ⊢ c ∈ R → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c = if c = d F ⁡ d − 1 F ⁡ c
123 122 ad2antrl ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c = if c = d F ⁡ d − 1 F ⁡ c
124 123 breq1d ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ↔ if c = d F ⁡ d − 1 F ⁡ c ≤ v
125 124 anbi1d ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c ↔ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c
126 1 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → M ∈ ℕ
127 2 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → R ∈ Fin
128 3 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → F : R ⟶ ℕ
129 5 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → G : R ⟶ ℕ 0
130 6 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → M − 1 Ramsey G ∈ ℕ 0
131 8 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → S ∈ Fin
132 9 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → S = M − 1 Ramsey G + 1
133 10 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → K : S C M ⟶ R
134 11 ad2antrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → X ∈ S
135 83 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → d ∈ R
136 110 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → w ⊆ S ∖ X
137 106 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → G ⁡ d ≤ w
138 simprrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → w C M − 1 ⊆ H -1 d
139 138 adantr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → w C M − 1 ⊆ H -1 d
140 simprll ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → c ∈ R
141 simprlr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → v ∈ 𝒫 w
142 141 elpwid ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → v ⊆ w
143 simprrl ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → if c = d F ⁡ d − 1 F ⁡ c ≤ v
144 simprrr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → v C M ⊆ K ↾ w C M -1 c
145 cnvresima ⊢ K ↾ w C M -1 c = K -1 c ∩ w C M
146 inss1 ⊢ K -1 c ∩ w C M ⊆ K -1 c
147 145 146 eqsstri ⊢ K ↾ w C M -1 c ⊆ K -1 c
148 144 147 sstrdi ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → v C M ⊆ K -1 c
149 126 127 128 4 129 130 7 131 132 133 134 12 135 136 137 139 140 142 143 148 ramub1lem1 ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w ∧ if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
150 149 expr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → if c = d F ⁡ d − 1 F ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
151 125 150 sylbid ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
152 151 anassrs ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R ∧ v ∈ 𝒫 w → y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
153 152 rexlimdva ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d ∧ c ∈ R → ∃ v ∈ 𝒫 w y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
154 153 reximdva ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → ∃ c ∈ R ∃ v ∈ 𝒫 w y ∈ R ⟼ if y = d F ⁡ d − 1 F ⁡ y ⁡ c ≤ v ∧ v C M ⊆ K ↾ w C M -1 c → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
155 115 154 mpd ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X ∧ G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
156 155 expr ⊢ φ ∧ d ∈ R ∧ w ∈ 𝒫 S ∖ X → G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
157 156 rexlimdvva ⊢ φ → ∃ d ∈ R ∃ w ∈ 𝒫 S ∖ X G ⁡ d ≤ w ∧ w C M − 1 ⊆ H -1 d → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c
158 79 157 mpd ⊢ φ → ∃ c ∈ R ∃ z ∈ 𝒫 S F ⁡ c ≤ z ∧ z C M ⊆ K -1 c