Theorem mreexd 17701

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 5302	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
5		mreexd.4	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
6	5	adantr 485	. . . 4 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑌 ∈ 𝑋)
7		mreexd.5	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
8	7	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
9		simplr 780	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑠 = 𝑆)
10		simpr 489	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌)
11	10	sneqd 4606	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → {𝑦} = {𝑌})
12	9, 11	uneq12d 4131	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑠 ∪ {𝑦}) = (𝑆 ∪ {𝑌}))
13	12	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘(𝑠 ∪ {𝑦})) = (𝑁‘(𝑆 ∪ {𝑌})))
14	8, 13	eleqtrrd 2873	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑠 ∪ {𝑦})))
15		mreexd.6	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))
16	15	ad2antrr 738	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑆))
17	9	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘𝑠) = (𝑁‘𝑆))
18	16, 17	neleqtrrd 2893	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑠))
19	14, 18	eldifd 3924	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠)))
20		simplr 780	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
21		simpllr 787	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑠 = 𝑆)
22		simpr 489	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
23	22	sneqd 4606	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → {𝑧} = {𝑍})
24	21, 23	uneq12d 4131	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑠 ∪ {𝑧}) = (𝑆 ∪ {𝑍}))
25	24	fveq2d 6889	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑁‘(𝑠 ∪ {𝑧})) = (𝑁‘(𝑆 ∪ {𝑍})))
26	20, 25	eleq12d 2864	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) ↔ 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
27	19, 26	rspcdv 3581	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
28	6, 27	rspcimdv 3579	. . 3 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
29	4, 28	rspcimdv 3579	. 2 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
30	1, 29	mpd 16	1 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 400   = wceq 1568   ∈ wcel 2150  ∀wral 3086   ∖ cdif 3910   ∪ cun 3911   ⊆ wss 3913  𝒫 cpw 4567  {csn 4594  ‘cfv 6540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-ext 2742  ax-sep 5262

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-sb 2099  df-clab 2749  df-cleq 2762  df-clel 2845  df-ral 3087  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-iota 6496  df-fv 6548

This theorem is referenced by:  mreexmrid  17702