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

Theorem mreexexlemd 16225
 Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16229. (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 791 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓)
65breq1d 4623 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝐾𝑓𝐾))
7 simpr 477 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔)
87breq1d 4623 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝐾𝑔𝐾))
96, 8orbi12d 745 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝐾𝑣𝐾) ↔ (𝑓𝐾𝑔𝐾)))
10 simpll 789 . . . . . . . . . . . 12 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = )
117, 10uneq12d 3746 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝑡) = (𝑔))
1211fveq2d 6152 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣𝑡)) = (𝑁‘(𝑔)))
135, 12sseq12d 3613 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔))))
145, 10uneq12d 3746 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝑡) = (𝑓))
1514eleq1d 2683 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝑡) ∈ 𝐼 ↔ (𝑓) ∈ 𝐼))
169, 13, 153anbi123d 1396 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) ↔ ((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
17 simpllr 798 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓)
18 simpr 477 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
1917, 18breq12d 4626 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢𝑖𝑓𝑗))
20 simplll 797 . . . . . . . . . . . 12 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = )
2118, 20uneq12d 3746 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖𝑡) = (𝑗))
2221eleq1d 2683 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖𝑡) ∈ 𝐼 ↔ (𝑗) ∈ 𝐼))
2319, 22anbi12d 746 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ (𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
24 simplr 791 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔)
2524pweqd 4135 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔)
2623, 25cbvrexdva2 3164 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
2716, 26imbi12d 334 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
28 simpl 473 . . . . . . . . . 10 ((𝑡 = 𝑢 = 𝑓) → 𝑡 = )
2928difeq2d 3706 . . . . . . . . 9 ((𝑡 = 𝑢 = 𝑓) → (𝑋𝑡) = (𝑋))
3029pweqd 4135 . . . . . . . 8 ((𝑡 = 𝑢 = 𝑓) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3130adantr 481 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3227, 31cbvraldva2 3163 . . . . . 6 ((𝑡 = 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3332, 30cbvraldva2 3163 . . . . 5 (𝑡 = → (∀𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3433cbvalv 2272 . . . 4 (∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
354, 34sylib 208 . . 3 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
36 ssun2 3755 . . . . . 6 𝐻 ⊆ (𝐹𝐻)
3736a1i 11 . . . . 5 (𝜑𝐻 ⊆ (𝐹𝐻))
383, 37ssexd 4765 . . . 4 (𝜑𝐻 ∈ V)
39 mreexexlemd.1 . . . . . . . . 9 (𝜑𝑋𝐽)
40 difexg 4768 . . . . . . . . 9 (𝑋𝐽 → (𝑋𝐻) ∈ V)
4139, 40syl 17 . . . . . . . 8 (𝜑 → (𝑋𝐻) ∈ V)
42 mreexexlemd.2 . . . . . . . 8 (𝜑𝐹 ⊆ (𝑋𝐻))
4341, 42sselpwd 4767 . . . . . . 7 (𝜑𝐹 ∈ 𝒫 (𝑋𝐻))
4443adantr 481 . . . . . 6 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋𝐻))
45 simpr 477 . . . . . . . 8 ((𝜑 = 𝐻) → = 𝐻)
4645difeq2d 3706 . . . . . . 7 ((𝜑 = 𝐻) → (𝑋) = (𝑋𝐻))
4746pweqd 4135 . . . . . 6 ((𝜑 = 𝐻) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
4844, 47eleqtrrd 2701 . . . . 5 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋))
49 mreexexlemd.3 . . . . . . . . 9 (𝜑𝐺 ⊆ (𝑋𝐻))
5041, 49sselpwd 4767 . . . . . . . 8 (𝜑𝐺 ∈ 𝒫 (𝑋𝐻))
5150ad2antrr 761 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋𝐻))
5247adantr 481 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
5351, 52eleqtrrd 2701 . . . . . 6 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋))
54 simplr 791 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
5554breq1d 4623 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝐾𝐹𝐾))
56 simpr 477 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
5756breq1d 4623 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝐾𝐺𝐾))
5855, 57orbi12d 745 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝐾𝑔𝐾) ↔ (𝐹𝐾𝐺𝐾)))
59 simpllr 798 . . . . . . . . . . 11 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
6056, 59uneq12d 3746 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔) = (𝐺𝐻))
6160fveq2d 6152 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔)) = (𝑁‘(𝐺𝐻)))
6254, 61sseq12d 3613 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔)) ↔ 𝐹 ⊆ (𝑁‘(𝐺𝐻))))
6354, 59uneq12d 3746 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓) = (𝐹𝐻))
6463eleq1d 2683 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓) ∈ 𝐼 ↔ (𝐹𝐻) ∈ 𝐼))
6558, 62, 643anbi123d 1396 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼)))
6656pweqd 4135 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺)
6754breq1d 4623 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑗𝐹𝑗))
6859uneq2d 3745 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗) = (𝑗𝐻))
6968eleq1d 2683 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗) ∈ 𝐼 ↔ (𝑗𝐻) ∈ 𝐼))
7067, 69anbi12d 746 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ (𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7166, 70rexeqbidv 3142 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7265, 71imbi12d 334 . . . . . 6 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) ↔ (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7353, 72rspcdv 3298 . . . . 5 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7448, 73rspcimdv 3296 . . . 4 ((𝜑 = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7538, 74spcimdv 3276 . . 3 (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7635, 75mpd 15 . 2 (𝜑 → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
771, 2, 3, 76mp3and 1424 1 (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∨ wo 383   ∧ wa 384   ∧ w3a 1036  ∀wal 1478   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∃wrex 2908  Vcvv 3186   ∖ cdif 3552   ∪ cun 3553   ⊆ wss 3555  𝒫 cpw 4130   class class class wbr 4613  ‘cfv 5847   ≈ cen 7896 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741 This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-iota 5810  df-fv 5855 This theorem is referenced by:  mreexexlem4d  16228  mreexexd  16229  mreexexdOLD  16230
 Copyright terms: Public domain W3C validator