Theorem mreexd 17816

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 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 5289	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
5		mreexd.4	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
6	5	adantr 486	. . . 4 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑌 ∈ 𝑋)
7		mreexd.5	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
8	7	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
9		simplr 781	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑠 = 𝑆)
10		simpr 490	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌)
11	10	sneqd 4595	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → {𝑦} = {𝑌})
12	9, 11	uneq12d 4168	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑠 ∪ {𝑦}) = (𝑆 ∪ {𝑌}))
13	12	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘(𝑠 ∪ {𝑦})) = (𝑁‘(𝑆 ∪ {𝑌})))
14	8, 13	eleqtrrd 2863	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑠 ∪ {𝑦})))
15		mreexd.6	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))
16	15	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑆))
17	9	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘𝑠) = (𝑁‘𝑆))
18	16, 17	neleqtrrd 2883	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑠))
19	14, 18	eldifd 4050	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠)))
20		simplr 781	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
21		simpllr 788	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑠 = 𝑆)
22		simpr 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
23	22	sneqd 4595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → {𝑧} = {𝑍})
24	21, 23	uneq12d 4168	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑠 ∪ {𝑧}) = (𝑆 ∪ {𝑍}))
25	24	fveq2d 6889	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑁‘(𝑠 ∪ {𝑧})) = (𝑁‘(𝑆 ∪ {𝑍})))
26	20, 25	eleq12d 2854	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) ↔ 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
27	19, 26	rspcdv 3568	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
28	6, 27	rspcimdv 3566	. . 3 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
29	4, 28	rspcimdv 3566	. 2 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
30	1, 29	mpd 16	1 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076   ⊆ wss 3895   ∖ cdif 4045   ∪ cun 4149  𝒫 cpw 4556  {csn 4583  ‘cfv 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ral 3077  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-br 5103  df-iota 6494  df-fv 6546

This theorem is used by:  mreexmrid  17817