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 5290	. . 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 4596	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → {𝑦} = {𝑌})
12	9, 11	uneq12d 4116	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑠 ∪ {𝑦}) = (𝑆 ∪ {𝑌}))
13	12	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘(𝑠 ∪ {𝑦})) = (𝑁‘(𝑆 ∪ {𝑌})))
14	8, 13	eleqtrrd 2864	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑠 ∪ {𝑦})))
15		mreexd.6	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))
16	15	ad2antrr 739	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑆))
17	9	fveq2d 6889	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘𝑠) = (𝑁‘𝑆))
18	16, 17	neleqtrrd 2884	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑠))
19	14, 18	eldifd 3910	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠)))
20		simplr 781	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
21		simpllr 788	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑠 = 𝑆)
22		simpr 490	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
23	22	sneqd 4596	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → {𝑧} = {𝑍})
24	21, 23	uneq12d 4116	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑠 ∪ {𝑧}) = (𝑆 ∪ {𝑍}))
25	24	fveq2d 6889	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑁‘(𝑠 ∪ {𝑧})) = (𝑁‘(𝑆 ∪ {𝑍})))
26	20, 25	eleq12d 2855	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) ↔ 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
27	19, 26	rspcdv 3569	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
28	6, 27	rspcimdv 3567	. . 3 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
29	4, 28	rspcimdv 3567	. 2 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
30	1, 29	mpd 16	1 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145  ∀wral 3077   ∖ cdif 3896   ∪ cun 3897   ⊆ wss 3899  𝒫 cpw 4557  {csn 4584  ‘cfv 6538

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249

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-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-ral 3078  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-iota 6494  df-fv 6546

This theorem is used by:  mreexmrid  17817