Theorem mreexexlem2d 17860

Description: Used in mreexexlem4d 17862 to prove the induction step in mreexexd 17863. See the proof of Proposition 4.2.1 in [FaureFrolicher] p. 86 to 87. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
mreexexlem2d.1	⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
mreexexlem2d.2	⊢ 𝑁 = (mrCls‘𝐴)
mreexexlem2d.3	⊢ 𝐼 = (mrInd‘𝐴)
mreexexlem2d.4	⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
mreexexlem2d.5	⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
mreexexlem2d.6	⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
mreexexlem2d.7	⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
mreexexlem2d.8	⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
mreexexlem2d.9	⊢ (𝜑 → 𝑌 ∈ 𝐹)

Assertion

Ref	Expression
mreexexlem2d	⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))

Distinct variable groups:   𝐹,𝑠,𝑔,𝑦,𝑧   𝐺,𝑠,𝑔,𝑦,𝑧   𝐻,𝑠,𝑔,𝑦,𝑧   𝜑,𝑠,𝑔,𝑦,𝑧   𝑌,𝑠,𝑔,𝑦,𝑧   𝑁,𝑠,𝑔,𝑦,𝑧   𝑋,𝑠,𝑦

Allowed substitution hints:   𝐴(𝑦, 𝑧, 𝑔, 𝑠)   𝐼(𝑦, 𝑧, 𝑔, 𝑠)   𝑋(𝑧, 𝑔)

Proof of Theorem mreexexlem2d

Step	Hyp	Ref	Expression
1		mreexexlem2d.7	. . . . . . . 8 ⊢ (𝜑 → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
2	1	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐹 ⊆ (𝑁‘(𝐺 ∪ 𝐻)))
3		mreexexlem2d.1	. . . . . . . . . 10 ⊢ (𝜑 → 𝐴 ∈ (Moore‘𝑋))
4	3	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐴 ∈ (Moore‘𝑋))
5		mreexexlem2d.2	. . . . . . . . 9 ⊢ 𝑁 = (mrCls‘𝐴)
6		simpr 490	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
7		ssun2 4180	. . . . . . . . . . . . 13 ⊢ 𝐻 ⊆ ((𝐹 ∖ {𝑌}) ∪ 𝐻)
8		difundir 4239	. . . . . . . . . . . . . 14 ⊢ ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∖ {𝑌}))
9		mreexexlem2d.9	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝑌 ∈ 𝐹)
10		incom 4109	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐹 ∩ 𝐻) = (𝐻 ∩ 𝐹)
11		mreexexlem2d.5	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝜑 → 𝐹 ⊆ (𝑋 ∖ 𝐻))
12		ssdifin0 4444	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐹 ⊆ (𝑋 ∖ 𝐻) → (𝐹 ∩ 𝐻) = ∅)
13	11, 12	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (𝐹 ∩ 𝐻) = ∅)
14	10, 13	eqtr3id 2812	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → (𝐻 ∩ 𝐹) = ∅)
15		minel 4422	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑌 ∈ 𝐹 ∧ (𝐻 ∩ 𝐹) = ∅) → ¬ 𝑌 ∈ 𝐻)
16	9, 14, 15	syl2anc 596	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ¬ 𝑌 ∈ 𝐻)
17		difsnb 4769	. . . . . . . . . . . . . . . 16 ⊢ (¬ 𝑌 ∈ 𝐻 ↔ (𝐻 ∖ {𝑌}) = 𝐻)
18	16, 17	sylib 221	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐻 ∖ {𝑌}) = 𝐻)
19	18	uneq2d 4170	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∖ {𝑌})) = ((𝐹 ∖ {𝑌}) ∪ 𝐻))
20	8, 19	eqtrid 2810	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ 𝐻))
21	7, 20	sseqtrrid 3956	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐻 ⊆ ((𝐹 ∪ 𝐻) ∖ {𝑌}))
22		mreexexlem2d.3	. . . . . . . . . . . . . . 15 ⊢ 𝐼 = (mrInd‘𝐴)
23		mreexexlem2d.8	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐹 ∪ 𝐻) ∈ 𝐼)
24	22, 3, 23	mrissd 17851	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝐹 ∪ 𝐻) ⊆ 𝑋)
25	24	ssdifssd 4086	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ 𝑋)
26	3, 5, 25	mrcssidd 17840	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
27	21, 26	sstrd 3923	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐻 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
28	27	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐻 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
29	6, 28	unssd 4193	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝐺 ∪ 𝐻) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
30	4, 5	mrcssvd 17838	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) ⊆ 𝑋)
31	4, 5, 29, 30	mrcssd 17839	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝐺 ∪ 𝐻)) ⊆ (𝑁‘(𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))))
32	25	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ((𝐹 ∪ 𝐻) ∖ {𝑌}) ⊆ 𝑋)
33	4, 5, 32	mrcidmd 17841	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) = (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
34	31, 33	sseqtrd 3949	. . . . . . 7 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑁‘(𝐺 ∪ 𝐻)) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
35	2, 34	sstrd 3923	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝐹 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
36	9	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ 𝐹)
37	35, 36	sseldd 3914	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
38	23	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝐹 ∪ 𝐻) ∈ 𝐼)
39		ssun1 4179	. . . . . . 7 ⊢ 𝐹 ⊆ (𝐹 ∪ 𝐻)
40	39, 36	sselid 3911	. . . . . 6 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → 𝑌 ∈ (𝐹 ∪ 𝐻))
41	5, 22, 4, 38, 40	ismri2dad 17852	. . . . 5 ⊢ ((𝜑 ∧ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ¬ 𝑌 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
42	37, 41	pm2.65da 829	. . . 4 ⊢ (𝜑 → ¬ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
43		nss 3977	. . . 4 ⊢ (¬ 𝐺 ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) ↔ ∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))))
44	42, 43	sylib 221	. . 3 ⊢ (𝜑 → ∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))))
45		simprl 783	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝑔 ∈ 𝐺)
46		ssun1 4179	. . . . . . . . . 10 ⊢ (𝐹 ∖ {𝑌}) ⊆ ((𝐹 ∖ {𝑌}) ∪ 𝐻)
47	46, 20	sseqtrrid 3956	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 ∖ {𝑌}) ⊆ ((𝐹 ∪ 𝐻) ∖ {𝑌}))
48	47, 26	sstrd 3923	. . . . . . . 8 ⊢ (𝜑 → (𝐹 ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
49	48	adantr 486	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝐹 ∖ {𝑌}) ⊆ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
50		simprr 785	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))
51	49, 50	ssneldd 3916	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝐹 ∖ {𝑌}))
52		unass 4173	. . . . . . 7 ⊢ (((𝐹 ∖ {𝑌}) ∪ 𝐻) ∪ {𝑔}) = ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔}))
53	3	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐴 ∈ (Moore‘𝑋))
54		mreexexlem2d.4	. . . . . . . . 9 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
55	54	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
56	23	adantr 486	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝐹 ∪ 𝐻) ∈ 𝐼)
57		difss 4075	. . . . . . . . . 10 ⊢ (𝐹 ∖ {𝑌}) ⊆ 𝐹
58		unss1 4186	. . . . . . . . . 10 ⊢ ((𝐹 ∖ {𝑌}) ⊆ 𝐹 → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ⊆ (𝐹 ∪ 𝐻))
59	57, 58	mp1i 14	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ⊆ (𝐹 ∪ 𝐻))
60	53, 5, 22, 56, 59	mrissmrid 17856	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ 𝐻) ∈ 𝐼)
61		mreexexlem2d.6	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ⊆ (𝑋 ∖ 𝐻))
62	61	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐺 ⊆ (𝑋 ∖ 𝐻))
63	62	difss2d 4078	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝐺 ⊆ 𝑋)
64	63, 45	sseldd 3914	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → 𝑔 ∈ 𝑋)
65	20	adantr 486	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∪ 𝐻) ∖ {𝑌}) = ((𝐹 ∖ {𝑌}) ∪ 𝐻))
66	65	fveq2d 6918	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})) = (𝑁‘((𝐹 ∖ {𝑌}) ∪ 𝐻)))
67	50, 66	neleqtrd 2886	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ¬ 𝑔 ∈ (𝑁‘((𝐹 ∖ {𝑌}) ∪ 𝐻)))
68	53, 5, 22, 55, 60, 64, 67	mreexmrid 17858	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (((𝐹 ∖ {𝑌}) ∪ 𝐻) ∪ {𝑔}) ∈ 𝐼)
69	52, 68	eqeltrrid 2869	. . . . . 6 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)
70	45, 51, 69	jca32 525	. . . . 5 ⊢ ((𝜑 ∧ (𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌})))) → (𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)))
71	70	ex 418	. . . 4 ⊢ (𝜑 → ((𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → (𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))))
72	71	eximdv 1952	. . 3 ⊢ (𝜑 → (∃𝑔(𝑔 ∈ 𝐺 ∧ ¬ 𝑔 ∈ (𝑁‘((𝐹 ∪ 𝐻) ∖ {𝑌}))) → ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))))
73	44, 72	mpd 16	. 2 ⊢ (𝜑 → ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)))
74		df-rex 3091	. 2 ⊢ (∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼) ↔ ∃𝑔(𝑔 ∈ 𝐺 ∧ (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼)))
75	73, 74	sylibr 237	1 ⊢ (𝜑 → ∃𝑔 ∈ 𝐺 (¬ 𝑔 ∈ (𝐹 ∖ {𝑌}) ∧ ((𝐹 ∖ {𝑌}) ∪ (𝐻 ∪ {𝑔})) ∈ 𝐼))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∀wral 3080  ∃wrex 3090   ⊆ wss 3900   ∖ cdif 4048   ∩ cin 4092   ∪ cun 4152  ∅c0 4281  𝒫 cpw 4560  {csn 4588  ‘cfv 6564  Moorecmre 17793  mrClscmrc 17794  mrIndcmri 17795

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5253  ax-nul 5264  ax-pow 5332  ax-pr 5396  ax-un 7781

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-int 4911  df-br 5107  df-opab 5172  df-mpt 5191  df-id 5551  df-xp 5662  df-rel 5663  df-cnv 5664  df-co 5665  df-dm 5666  df-rn 5667  df-res 5668  df-ima 5669  df-iota 6518  df-fun 6566  df-fn 6567  df-f 6568  df-fv 6572  df-mre 17797  df-mrc 17798  df-mri 17799

This theorem is used by:  mreexexlem4d  17862