Theorem mreexd 16913

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 5230	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝒫 𝑋)
5		mreexd.4	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑋)
6	5	adantr 483	. . . 4 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → 𝑌 ∈ 𝑋)
7		mreexd.5	. . . . . . . 8 ⊢ (𝜑 → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
8	7	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑆 ∪ {𝑌})))
9		simplr 767	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑠 = 𝑆)
10		simpr 487	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑦 = 𝑌)
11	10	sneqd 4579	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → {𝑦} = {𝑌})
12	9, 11	uneq12d 4140	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑠 ∪ {𝑦}) = (𝑆 ∪ {𝑌}))
13	12	fveq2d 6674	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘(𝑠 ∪ {𝑦})) = (𝑁‘(𝑆 ∪ {𝑌})))
14	8, 13	eleqtrrd 2916	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ (𝑁‘(𝑠 ∪ {𝑦})))
15		mreexd.6	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘𝑆))
16	15	ad2antrr 724	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑆))
17	9	fveq2d 6674	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (𝑁‘𝑠) = (𝑁‘𝑆))
18	16, 17	neleqtrrd 2935	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → ¬ 𝑍 ∈ (𝑁‘𝑠))
19	14, 18	eldifd 3947	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → 𝑍 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠)))
20		simplr 767	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑦 = 𝑌)
21		simpllr 774	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑠 = 𝑆)
22		simpr 487	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → 𝑧 = 𝑍)
23	22	sneqd 4579	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → {𝑧} = {𝑍})
24	21, 23	uneq12d 4140	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑠 ∪ {𝑧}) = (𝑆 ∪ {𝑍}))
25	24	fveq2d 6674	. . . . . 6 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑁‘(𝑠 ∪ {𝑧})) = (𝑁‘(𝑆 ∪ {𝑍})))
26	20, 25	eleq12d 2907	. . . . 5 ⊢ ((((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) ∧ 𝑧 = 𝑍) → (𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) ↔ 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
27	19, 26	rspcdv 3615	. . . 4 ⊢ (((𝜑 ∧ 𝑠 = 𝑆) ∧ 𝑦 = 𝑌) → (∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
28	6, 27	rspcimdv 3613	. . 3 ⊢ ((𝜑 ∧ 𝑠 = 𝑆) → (∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
29	4, 28	rspcimdv 3613	. 2 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝑋∀𝑦 ∈ 𝑋 ∀𝑧 ∈ ((𝑁‘(𝑠 ∪ {𝑦})) ∖ (𝑁‘𝑠))𝑦 ∈ (𝑁‘(𝑠 ∪ {𝑧})) → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍}))))
30	1, 29	mpd 15	1 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘(𝑆 ∪ {𝑍})))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 398   = wceq 1537   ∈ wcel 2114  ∀wral 3138   ∖ cdif 3933   ∪ cun 3934   ⊆ wss 3936  𝒫 cpw 4539  {csn 4567  ‘cfv 6355

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4839  df-br 5067  df-iota 6314  df-fv 6363

This theorem is referenced by:  mreexmrid  16914