MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  mreexexlemd Structured version   Visualization version   GIF version

Theorem mreexexlemd 17615
Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 17619. (Contributed by David Moews, 1-May-2017.)
Hypotheses
Ref Expression
mreexexlemd.1 (𝜑𝑋𝐽)
mreexexlemd.2 (𝜑𝐹 ⊆ (𝑋𝐻))
mreexexlemd.3 (𝜑𝐺 ⊆ (𝑋𝐻))
mreexexlemd.4 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
mreexexlemd.5 (𝜑 → (𝐹𝐻) ∈ 𝐼)
mreexexlemd.6 (𝜑 → (𝐹𝐾𝐺𝐾))
mreexexlemd.7 (𝜑 → ∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)))
Assertion
Ref Expression
mreexexlemd (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Distinct variable groups:   𝑗,𝐹   𝑗,𝐺   𝑗,𝐻   𝜑,𝑗   𝑢,𝑡,𝑣,𝑖,𝐼,𝑗   𝑡,𝐾,𝑢,𝑣   𝑡,𝑁,𝑢,𝑣   𝑡,𝑋,𝑢,𝑣
Allowed substitution hints:   𝜑(𝑣,𝑢,𝑡,𝑖)   𝐹(𝑣,𝑢,𝑡,𝑖)   𝐺(𝑣,𝑢,𝑡,𝑖)   𝐻(𝑣,𝑢,𝑡,𝑖)   𝐽(𝑣,𝑢,𝑡,𝑖,𝑗)   𝐾(𝑖,𝑗)   𝑁(𝑖,𝑗)   𝑋(𝑖,𝑗)

Proof of Theorem mreexexlemd
Dummy variables 𝑓 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mreexexlemd.6 . 2 (𝜑 → (𝐹𝐾𝐺𝐾))
2 mreexexlemd.4 . 2 (𝜑𝐹 ⊆ (𝑁‘(𝐺𝐻)))
3 mreexexlemd.5 . 2 (𝜑 → (𝐹𝐻) ∈ 𝐼)
4 mreexexlemd.7 . . . 4 (𝜑 → ∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)))
5 simplr 768 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓)
65breq1d 5152 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝐾𝑓𝐾))
7 simpr 484 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔)
87breq1d 5152 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝐾𝑔𝐾))
96, 8orbi12d 917 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝐾𝑣𝐾) ↔ (𝑓𝐾𝑔𝐾)))
10 simpll 766 . . . . . . . . . . . 12 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = )
117, 10uneq12d 4160 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝑡) = (𝑔))
1211fveq2d 6895 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣𝑡)) = (𝑁‘(𝑔)))
135, 12sseq12d 4011 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔))))
145, 10uneq12d 4160 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝑡) = (𝑓))
1514eleq1d 2813 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝑡) ∈ 𝐼 ↔ (𝑓) ∈ 𝐼))
169, 13, 153anbi123d 1433 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) ↔ ((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
17 simpllr 775 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓)
18 simpr 484 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
1917, 18breq12d 5155 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢𝑖𝑓𝑗))
20 simplll 774 . . . . . . . . . . . 12 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = )
2118, 20uneq12d 4160 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖𝑡) = (𝑗))
2221eleq1d 2813 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖𝑡) ∈ 𝐼 ↔ (𝑗) ∈ 𝐼))
2319, 22anbi12d 630 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ (𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
24 simplr 768 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔)
2524pweqd 4615 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔)
2623, 25cbvrexdva2 3340 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
2716, 26imbi12d 344 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
28 simpl 482 . . . . . . . . . 10 ((𝑡 = 𝑢 = 𝑓) → 𝑡 = )
2928difeq2d 4118 . . . . . . . . 9 ((𝑡 = 𝑢 = 𝑓) → (𝑋𝑡) = (𝑋))
3029pweqd 4615 . . . . . . . 8 ((𝑡 = 𝑢 = 𝑓) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3130adantr 480 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3227, 31cbvraldva2 3339 . . . . . 6 ((𝑡 = 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3332, 30cbvraldva2 3339 . . . . 5 (𝑡 = → (∀𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3433cbvalvw 2032 . . . 4 (∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
354, 34sylib 217 . . 3 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
36 ssun2 4169 . . . . . 6 𝐻 ⊆ (𝐹𝐻)
3736a1i 11 . . . . 5 (𝜑𝐻 ⊆ (𝐹𝐻))
383, 37ssexd 5318 . . . 4 (𝜑𝐻 ∈ V)
39 mreexexlemd.1 . . . . . . . . 9 (𝜑𝑋𝐽)
4039difexd 5325 . . . . . . . 8 (𝜑 → (𝑋𝐻) ∈ V)
41 mreexexlemd.2 . . . . . . . 8 (𝜑𝐹 ⊆ (𝑋𝐻))
4240, 41sselpwd 5322 . . . . . . 7 (𝜑𝐹 ∈ 𝒫 (𝑋𝐻))
4342adantr 480 . . . . . 6 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋𝐻))
44 simpr 484 . . . . . . . 8 ((𝜑 = 𝐻) → = 𝐻)
4544difeq2d 4118 . . . . . . 7 ((𝜑 = 𝐻) → (𝑋) = (𝑋𝐻))
4645pweqd 4615 . . . . . 6 ((𝜑 = 𝐻) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
4743, 46eleqtrrd 2831 . . . . 5 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋))
48 mreexexlemd.3 . . . . . . . . 9 (𝜑𝐺 ⊆ (𝑋𝐻))
4940, 48sselpwd 5322 . . . . . . . 8 (𝜑𝐺 ∈ 𝒫 (𝑋𝐻))
5049ad2antrr 725 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋𝐻))
5146adantr 480 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
5250, 51eleqtrrd 2831 . . . . . 6 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋))
53 simplr 768 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
5453breq1d 5152 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝐾𝐹𝐾))
55 simpr 484 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
5655breq1d 5152 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝐾𝐺𝐾))
5754, 56orbi12d 917 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝐾𝑔𝐾) ↔ (𝐹𝐾𝐺𝐾)))
58 simpllr 775 . . . . . . . . . . 11 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
5955, 58uneq12d 4160 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔) = (𝐺𝐻))
6059fveq2d 6895 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔)) = (𝑁‘(𝐺𝐻)))
6153, 60sseq12d 4011 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔)) ↔ 𝐹 ⊆ (𝑁‘(𝐺𝐻))))
6253, 58uneq12d 4160 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓) = (𝐹𝐻))
6362eleq1d 2813 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓) ∈ 𝐼 ↔ (𝐹𝐻) ∈ 𝐼))
6457, 61, 633anbi123d 1433 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼)))
6555pweqd 4615 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺)
6653breq1d 5152 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑗𝐹𝑗))
6758uneq2d 4159 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗) = (𝑗𝐻))
6867eleq1d 2813 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗) ∈ 𝐼 ↔ (𝑗𝐻) ∈ 𝐼))
6966, 68anbi12d 630 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ (𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7065, 69rexeqbidv 3338 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7164, 70imbi12d 344 . . . . . 6 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) ↔ (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7252, 71rspcdv 3599 . . . . 5 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7347, 72rspcimdv 3597 . . . 4 ((𝜑 = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7438, 73spcimdv 3578 . . 3 (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7535, 74mpd 15 . 2 (𝜑 → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
761, 2, 3, 75mp3and 1461 1 (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wo 846  w3a 1085  wal 1532   = wceq 1534  wcel 2099  wral 3056  wrex 3065  Vcvv 3469  cdif 3941  cun 3942  wss 3944  𝒫 cpw 4598   class class class wbr 5142  cfv 6542  cen 8952
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698  ax-sep 5293
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-ral 3057  df-rex 3066  df-rab 3428  df-v 3471  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-br 5143  df-iota 6494  df-fv 6550
This theorem is referenced by:  mreexexlem4d  17618  mreexexd  17619
  Copyright terms: Public domain W3C validator