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

Theorem mreexexlemd 16351
Description: This lemma is used to generate substitution instances of the induction hypothesis in mreexexd 16355. (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 807 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑢 = 𝑓)
65breq1d 4695 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝐾𝑓𝐾))
7 simpr 476 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑣 = 𝑔)
87breq1d 4695 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝐾𝑔𝐾))
96, 8orbi12d 746 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝐾𝑣𝐾) ↔ (𝑓𝐾𝑔𝐾)))
10 simpll 805 . . . . . . . . . . . 12 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝑡 = )
117, 10uneq12d 3801 . . . . . . . . . . 11 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑣𝑡) = (𝑔))
1211fveq2d 6233 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑁‘(𝑣𝑡)) = (𝑁‘(𝑔)))
135, 12sseq12d 3667 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢 ⊆ (𝑁‘(𝑣𝑡)) ↔ 𝑓 ⊆ (𝑁‘(𝑔))))
145, 10uneq12d 3801 . . . . . . . . . 10 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (𝑢𝑡) = (𝑓))
1514eleq1d 2715 . . . . . . . . 9 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((𝑢𝑡) ∈ 𝐼 ↔ (𝑓) ∈ 𝐼))
169, 13, 153anbi123d 1439 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) ↔ ((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼)))
17 simpllr 815 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑢 = 𝑓)
18 simpr 476 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑖 = 𝑗)
1917, 18breq12d 4698 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑢𝑖𝑓𝑗))
20 simplll 813 . . . . . . . . . . . 12 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑡 = )
2118, 20uneq12d 3801 . . . . . . . . . . 11 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → (𝑖𝑡) = (𝑗))
2221eleq1d 2715 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑖𝑡) ∈ 𝐼 ↔ (𝑗) ∈ 𝐼))
2319, 22anbi12d 747 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → ((𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ (𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
24 simplr 807 . . . . . . . . . 10 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝑣 = 𝑔)
2524pweqd 4196 . . . . . . . . 9 ((((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) ∧ 𝑖 = 𝑗) → 𝒫 𝑣 = 𝒫 𝑔)
2623, 25cbvrexdva2 3206 . . . . . . . 8 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → (∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
2716, 26imbi12d 333 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → ((((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
28 simpl 472 . . . . . . . . . 10 ((𝑡 = 𝑢 = 𝑓) → 𝑡 = )
2928difeq2d 3761 . . . . . . . . 9 ((𝑡 = 𝑢 = 𝑓) → (𝑋𝑡) = (𝑋))
3029pweqd 4196 . . . . . . . 8 ((𝑡 = 𝑢 = 𝑓) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3130adantr 480 . . . . . . 7 (((𝑡 = 𝑢 = 𝑓) ∧ 𝑣 = 𝑔) → 𝒫 (𝑋𝑡) = 𝒫 (𝑋))
3227, 31cbvraldva2 3205 . . . . . 6 ((𝑡 = 𝑢 = 𝑓) → (∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3332, 30cbvraldva2 3205 . . . . 5 (𝑡 = → (∀𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼))))
3433cbvalv 2309 . . . 4 (∀𝑡𝑢 ∈ 𝒫 (𝑋𝑡)∀𝑣 ∈ 𝒫 (𝑋𝑡)(((𝑢𝐾𝑣𝐾) ∧ 𝑢 ⊆ (𝑁‘(𝑣𝑡)) ∧ (𝑢𝑡) ∈ 𝐼) → ∃𝑖 ∈ 𝒫 𝑣(𝑢𝑖 ∧ (𝑖𝑡) ∈ 𝐼)) ↔ ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
354, 34sylib 208 . . 3 (𝜑 → ∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)))
36 ssun2 3810 . . . . . 6 𝐻 ⊆ (𝐹𝐻)
3736a1i 11 . . . . 5 (𝜑𝐻 ⊆ (𝐹𝐻))
383, 37ssexd 4838 . . . 4 (𝜑𝐻 ∈ V)
39 mreexexlemd.1 . . . . . . . . 9 (𝜑𝑋𝐽)
40 difexg 4841 . . . . . . . . 9 (𝑋𝐽 → (𝑋𝐻) ∈ V)
4139, 40syl 17 . . . . . . . 8 (𝜑 → (𝑋𝐻) ∈ V)
42 mreexexlemd.2 . . . . . . . 8 (𝜑𝐹 ⊆ (𝑋𝐻))
4341, 42sselpwd 4840 . . . . . . 7 (𝜑𝐹 ∈ 𝒫 (𝑋𝐻))
4443adantr 480 . . . . . 6 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋𝐻))
45 simpr 476 . . . . . . . 8 ((𝜑 = 𝐻) → = 𝐻)
4645difeq2d 3761 . . . . . . 7 ((𝜑 = 𝐻) → (𝑋) = (𝑋𝐻))
4746pweqd 4196 . . . . . 6 ((𝜑 = 𝐻) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
4844, 47eleqtrrd 2733 . . . . 5 ((𝜑 = 𝐻) → 𝐹 ∈ 𝒫 (𝑋))
49 mreexexlemd.3 . . . . . . . . 9 (𝜑𝐺 ⊆ (𝑋𝐻))
5041, 49sselpwd 4840 . . . . . . . 8 (𝜑𝐺 ∈ 𝒫 (𝑋𝐻))
5150ad2antrr 762 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋𝐻))
5247adantr 480 . . . . . . 7 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝒫 (𝑋) = 𝒫 (𝑋𝐻))
5351, 52eleqtrrd 2733 . . . . . 6 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → 𝐺 ∈ 𝒫 (𝑋))
54 simplr 807 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
5554breq1d 4695 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝐾𝐹𝐾))
56 simpr 476 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
5756breq1d 4695 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝐾𝐺𝐾))
5855, 57orbi12d 746 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝐾𝑔𝐾) ↔ (𝐹𝐾𝐺𝐾)))
59 simpllr 815 . . . . . . . . . . 11 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
6056, 59uneq12d 3801 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔) = (𝐺𝐻))
6160fveq2d 6233 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑁‘(𝑔)) = (𝑁‘(𝐺𝐻)))
6254, 61sseq12d 3667 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓 ⊆ (𝑁‘(𝑔)) ↔ 𝐹 ⊆ (𝑁‘(𝐺𝐻))))
6354, 59uneq12d 3801 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓) = (𝐹𝐻))
6463eleq1d 2715 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓) ∈ 𝐼 ↔ (𝐹𝐻) ∈ 𝐼))
6558, 62, 643anbi123d 1439 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) ↔ ((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼)))
6656pweqd 4196 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝒫 𝑔 = 𝒫 𝐺)
6754breq1d 4695 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑗𝐹𝑗))
6859uneq2d 3800 . . . . . . . . . 10 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑗) = (𝑗𝐻))
6968eleq1d 2715 . . . . . . . . 9 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑗) ∈ 𝐼 ↔ (𝑗𝐻) ∈ 𝐼))
7067, 69anbi12d 747 . . . . . . . 8 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ (𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7166, 70rexeqbidv 3183 . . . . . . 7 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼) ↔ ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
7265, 71imbi12d 333 . . . . . 6 ((((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) ↔ (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7353, 72rspcdv 3343 . . . . 5 (((𝜑 = 𝐻) ∧ 𝑓 = 𝐹) → (∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7448, 73rspcimdv 3341 . . . 4 ((𝜑 = 𝐻) → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7538, 74spcimdv 3321 . . 3 (𝜑 → (∀𝑓 ∈ 𝒫 (𝑋)∀𝑔 ∈ 𝒫 (𝑋)(((𝑓𝐾𝑔𝐾) ∧ 𝑓 ⊆ (𝑁‘(𝑔)) ∧ (𝑓) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝑔(𝑓𝑗 ∧ (𝑗) ∈ 𝐼)) → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))))
7635, 75mpd 15 . 2 (𝜑 → (((𝐹𝐾𝐺𝐾) ∧ 𝐹 ⊆ (𝑁‘(𝐺𝐻)) ∧ (𝐹𝐻) ∈ 𝐼) → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼)))
771, 2, 3, 76mp3and 1467 1 (𝜑 → ∃𝑗 ∈ 𝒫 𝐺(𝐹𝑗 ∧ (𝑗𝐻) ∈ 𝐼))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wo 382  wa 383  w3a 1054  wal 1521   = wceq 1523  wcel 2030  wral 2941  wrex 2942  Vcvv 3231  cdif 3604  cun 3605  wss 3607  𝒫 cpw 4191   class class class wbr 4685  cfv 5926  cen 7994
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ral 2946  df-rex 2947  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-br 4686  df-iota 5889  df-fv 5934
This theorem is referenced by:  mreexexlem4d  16354  mreexexd  16355  mreexexdOLD  16356
  Copyright terms: Public domain W3C validator