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

Theorem mreexexlemd 16732
Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16736. (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 765 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓)
65breq1d 4966 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝐾𝑓𝐾))
7 simpr 485 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔)
87breq1d 4966 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝐾𝑔𝐾))
96, 8orbi12d 911 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝐾𝑣𝐾) ↔ (𝑓𝐾𝑔𝐾)))
10 simpll 763 . . . . . . . . . . . 12 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = )
117, 10uneq12d 4056 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝑡) = (𝑔))
1211fveq2d 6534 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣𝑡)) = (𝑁‘(𝑔)))
135, 12sseq12d 3916 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔))))
145, 10uneq12d 4056 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝑡) = (𝑓))
1514eleq1d 2865 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝑡) ∈ 𝐼 ↔ (𝑓) ∈ 𝐼))
169, 13, 153anbi123d 1426 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) ↔ ((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
17 simpllr 772 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓)
18 simpr 485 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
1917, 18breq12d 4969 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢𝑖𝑓𝑗))
20 simplll 771 . . . . . . . . . . . 12 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = )
2118, 20uneq12d 4056 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖𝑡) = (𝑗))
2221eleq1d 2865 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖𝑡) ∈ 𝐼 ↔ (𝑗) ∈ 𝐼))
2319, 22anbi12d 630 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ (𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
24 simplr 765 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔)
2524pweqd 4452 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔)
2623, 25cbvrexdva2 3405 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
2716, 26imbi12d 346 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
28 simpl 483 . . . . . . . . . 10 ((𝑡 = 𝑢 = 𝑓) → 𝑡 = )
2928difeq2d 4015 . . . . . . . . 9 ((𝑡 = 𝑢 = 𝑓) → (𝑋𝑡) = (𝑋))
3029pweqd 4452 . . . . . . . 8 ((𝑡 = 𝑢 = 𝑓) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3130adantr 481 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3227, 31cbvraldva2 3404 . . . . . 6 ((𝑡 = 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3332, 30cbvraldva2 3404 . . . . 5 (𝑡 = → (∀𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3433cbvalvw 2018 . . . 4 (∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
354, 34sylib 219 . . 3 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
36 ssun2 4065 . . . . . 6 𝐻 ⊆ (𝐹𝐻)
3736a1i 11 . . . . 5 (𝜑𝐻 ⊆ (𝐹𝐻))
383, 37ssexd 5112 . . . 4 (𝜑𝐻 ∈ V)
39 mreexexlemd.1 . . . . . . . . 9 (𝜑𝑋𝐽)
40 difexg 5115 . . . . . . . . 9 (𝑋𝐽 → (𝑋𝐻) ∈ V)
4139, 40syl 17 . . . . . . . 8 (𝜑 → (𝑋𝐻) ∈ V)
42 mreexexlemd.2 . . . . . . . 8 (𝜑𝐹 ⊆ (𝑋𝐻))
4341, 42sselpwd 5114 . . . . . . 7 (𝜑𝐹 ∈ 𝒫 (𝑋𝐻))
4443adantr 481 . . . . . 6 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋𝐻))
45 simpr 485 . . . . . . . 8 ((𝜑 = 𝐻) → = 𝐻)
4645difeq2d 4015 . . . . . . 7 ((𝜑 = 𝐻) → (𝑋) = (𝑋𝐻))
4746pweqd 4452 . . . . . 6 ((𝜑 = 𝐻) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
4844, 47eleqtrrd 2884 . . . . 5 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋))
49 mreexexlemd.3 . . . . . . . . 9 (𝜑𝐺 ⊆ (𝑋𝐻))
5041, 49sselpwd 5114 . . . . . . . 8 (𝜑𝐺 ∈ 𝒫 (𝑋𝐻))
5150ad2antrr 722 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋𝐻))
5247adantr 481 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
5351, 52eleqtrrd 2884 . . . . . 6 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋))
54 simplr 765 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
5554breq1d 4966 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝐾𝐹𝐾))
56 simpr 485 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
5756breq1d 4966 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝐾𝐺𝐾))
5855, 57orbi12d 911 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝐾𝑔𝐾) ↔ (𝐹𝐾𝐺𝐾)))
59 simpllr 772 . . . . . . . . . . 11 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
6056, 59uneq12d 4056 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔) = (𝐺𝐻))
6160fveq2d 6534 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔)) = (𝑁‘(𝐺𝐻)))
6254, 61sseq12d 3916 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔)) ↔ 𝐹 ⊆ (𝑁‘(𝐺𝐻))))
6354, 59uneq12d 4056 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓) = (𝐹𝐻))
6463eleq1d 2865 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓) ∈ 𝐼 ↔ (𝐹𝐻) ∈ 𝐼))
6558, 62, 643anbi123d 1426 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼)))
6656pweqd 4452 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺)
6754breq1d 4966 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑗𝐹𝑗))
6859uneq2d 4055 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗) = (𝑗𝐻))
6968eleq1d 2865 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗) ∈ 𝐼 ↔ (𝑗𝐻) ∈ 𝐼))
7067, 69anbi12d 630 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ (𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7166, 70rexeqbidv 3359 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7265, 71imbi12d 346 . . . . . 6 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) ↔ (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7353, 72rspcdv 3557 . . . . 5 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7448, 73rspcimdv 3555 . . . 4 ((𝜑 = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7538, 74spcimdv 3530 . . 3 (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7635, 75mpd 15 . 2 (𝜑 → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
771, 2, 3, 76mp3and 1454 1 (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 842  w3a 1078  wal 1518   = wceq 1520  wcel 2079  wral 3103  wrex 3104  Vcvv 3432  cdif 3851  cun 3852  wss 3854  𝒫 cpw 4447   class class class wbr 4956  cfv 6217  cen 8344
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1775  ax-4 1789  ax-5 1886  ax-6 1945  ax-7 1990  ax-8 2081  ax-9 2089  ax-10 2110  ax-11 2124  ax-12 2139  ax-ext 2767  ax-sep 5088
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1080  df-tru 1523  df-ex 1760  df-nf 1764  df-sb 2041  df-clab 2774  df-cleq 2786  df-clel 2861  df-nfc 2933  df-ral 3108  df-rex 3109  df-rab 3112  df-v 3434  df-dif 3857  df-un 3859  df-in 3861  df-ss 3869  df-nul 4207  df-if 4376  df-pw 4449  df-sn 4467  df-pr 4469  df-op 4473  df-uni 4740  df-br 4957  df-iota 6181  df-fv 6225
This theorem is referenced by:  mreexexlem4d  16735  mreexexd  16736
  Copyright terms: Public domain W3C validator