Theorem mreexd 17268

Description: In a Moore system, the closure operator is said to have the exchange property if, for all elements 𝑦 and 𝑧 of the base set and subsets 𝑆 of the base set such that 𝑧 is in the closure of (𝑆 ∪ {𝑦}) but not in the closure of 𝑆, 𝑦 is in the closure of (𝑆 ∪ {𝑧}) (Definition 3.1.9 in [FaureFrolicher] p. 57 to 58.) This theorem allows us to construct substitution instances of this definition. (Contributed by David Moews, 1-May-2017.)

Hypotheses

Ref	Expression
mreexd.1	⊢ (𝜑 → 𝑋 ∈ 𝑉)
mreexd.2	⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
mreexd.3	⊢ (𝜑 → 𝑆 ⊆ 𝑋)
mreexd.4	⊢ (𝜑 → 𝑌 ∈ 𝑋)
mreexd.5	⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
mreexd.6	⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))

Assertion

Ref	Expression
mreexd	⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

Distinct variable groups:   𝑋,𝑠,𝑦   𝑆,𝑠,𝑧,𝑦   𝜑,𝑠,𝑦,𝑧   𝑌,𝑠,𝑦,𝑧   𝑍,𝑠,𝑦,𝑧   𝑁,𝑠,𝑦,𝑧

Allowed substitution hints:   𝑉(𝑦,𝑧,𝑠)   𝑋(𝑧)

Proof of Theorem mreexd

Step	Hyp	Ref	Expression
1		mreexd.2	. 2 ⊢ (𝜑 → ∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})))
2		mreexd.1	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
3		mreexd.3	. . . 4 ⊢ (𝜑 → 𝑆 ⊆ 𝑋)
4	2, 3	sselpwd 5245	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
5		mreexd.4	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
6	5	adantr 480	. . . 4 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑌 ∈ 𝑋)
7		mreexd.5	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
8	7	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
9		simplr 765	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑠 = 𝑆)
10		simpr 484	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌)
11	10	sneqd 4570	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → {𝑦} = {𝑌})
12	9, 11	uneq12d 4094	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑠 ∪ {𝑦}) = (𝑆 ∪ {𝑌}))
13	12	fveq2d 6760	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘(𝑠 ∪ {𝑦})) = (𝑁‘(𝑆 ∪ {𝑌})))
14	8, 13	eleqtrrd 2842	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑠 ∪ {𝑦})))
15		mreexd.6	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))
16	15	ad2antrr 722	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑆))
17	9	fveq2d 6760	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘𝑠) = (𝑁‘𝑆))
18	16, 17	neleqtrrd 2861	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑠))
19	14, 18	eldifd 3894	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠)))
20		simplr 765	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
21		simpllr 772	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑠 = 𝑆)
22		simpr 484	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
23	22	sneqd 4570	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → {𝑧} = {𝑍})
24	21, 23	uneq12d 4094	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑠 ∪ {𝑧}) = (𝑆 ∪ {𝑍}))
25	24	fveq2d 6760	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑁‘(𝑠 ∪ {𝑧})) = (𝑁‘(𝑆 ∪ {𝑍})))
26	20, 25	eleq12d 2833	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) ↔ 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
27	19, 26	rspcdv 3543	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
28	6, 27	rspcimdv 3541	. . 3 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
29	4, 28	rspcimdv 3541	. 2 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
30	1, 29	mpd 15	1 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108  ∀wral 3063   ∖ cdif 3880   ∪ cun 3881   ⊆ wss 3883  𝒫 cpw 4530  {csn 4558  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-ral 3068  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  mreexmrid  17269