ntrneix3

Description: The closure of the union of any pair is a subset of the union of closures if and only if the union of any pair belonging to the convergents of a point implies at least one of the pair belongs to the the convergents of that point. (Contributed by RP, 19-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
	ntrnei.f	$⊢ F = 𝒫 B O B$
	ntrnei.r	$⊢ φ \to I F N$
Assertion	ntrneix3	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		ntrnei.f	$⊢ F = 𝒫 B O B$
3		ntrnei.r	$⊢ φ \to I F N$
4		dfss3	$⊢ I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall x \in I (s \cup t) x \in (I (s) \cup I (t))$
5	1 2 3	ntrneiiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
6	5	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I \in ({𝒫 B}^{𝒫 B})$
7		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
8	6 7	syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I : 𝒫 B ⟶ 𝒫 B$
9	1 2 3	ntrneibex	$⊢ φ \to B \in V$
10	9	ad2antrr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to B \in V$
11		simplr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \in 𝒫 B$
12	11	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \subseteq B$
13		simpr	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to t \in 𝒫 B$
14	13	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to t \subseteq B$
15	12 14	unssd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \cup t \subseteq B$
16	10 15	sselpwd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to s \cup t \in 𝒫 B$
17	8 16	ffvelrnd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s \cup t) \in 𝒫 B$
18	17	elpwid	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to I (s \cup t) \subseteq B$
19		ralss	$⊢ I (s \cup t) \subseteq B \to (\forall x \in I (s \cup t) x \in (I (s) \cup I (t)) \leftrightarrow \forall x \in B (x \in I (s \cup t) \to x \in (I (s) \cup I (t))))$
20	18 19	syl	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in I (s \cup t) x \in (I (s) \cup I (t)) \leftrightarrow \forall x \in B (x \in I (s \cup t) \to x \in (I (s) \cup I (t))))$
21	3	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to I F N$
22		simpr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to x \in B$
23	9	ad3antrrr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to B \in V$
24		simpllr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \in 𝒫 B$
25	24	elpwid	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \subseteq B$
26		simplr	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \in 𝒫 B$
27	26	elpwid	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to t \subseteq B$
28	25 27	unssd	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \cup t \subseteq B$
29	23 28	sselpwd	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to s \cup t \in 𝒫 B$
30	1 2 21 22 29	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s \cup t) \leftrightarrow s \cup t \in N (x))$
31		elun	$⊢ x \in (I (s) \cup I (t)) \leftrightarrow (x \in I (s) \lor x \in I (t))$
32	1 2 21 22 24	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (s) \leftrightarrow s \in N (x))$
33	1 2 21 22 26	ntrneiel	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in I (t) \leftrightarrow t \in N (x))$
34	32 33	orbi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in I (s) \lor x \in I (t)) \leftrightarrow (s \in N (x) \lor t \in N (x)))$
35	31 34	syl5bb	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to (x \in (I (s) \cup I (t)) \leftrightarrow (s \in N (x) \lor t \in N (x)))$
36	30 35	imbi12d	$⊢ (((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \land x \in B) \to ((x \in I (s \cup t) \to x \in (I (s) \cup I (t))) \leftrightarrow (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
37	36	ralbidva	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in B (x \in I (s \cup t) \to x \in (I (s) \cup I (t))) \leftrightarrow \forall x \in B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
38	20 37	bitrd	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (\forall x \in I (s \cup t) x \in (I (s) \cup I (t)) \leftrightarrow \forall x \in B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
39	4 38	syl5bb	$⊢ ((φ \land s \in 𝒫 B) \land t \in 𝒫 B) \to (I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall x \in B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
40	39	ralbidva	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall t \in 𝒫 B \forall x \in B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
41		ralcom	$⊢ \forall t \in 𝒫 B \forall x \in B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))) \leftrightarrow \forall x \in B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x)))$
42	40 41	bitrdi	$⊢ (φ \land s \in 𝒫 B) \to (\forall t \in 𝒫 B I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall x \in B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
43	42	ralbidva	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$
44		ralcom	$⊢ \forall s \in 𝒫 B \forall x \in B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x)))$
45	43 44	bitrdi	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cup t) \subseteq I (s) \cup I (t) \leftrightarrow \forall x \in B \forall s \in 𝒫 B \forall t \in 𝒫 B (s \cup t \in N (x) \to (s \in N (x) \lor t \in N (x))))$

Metamath Proof Explorer

Theorem ntrneix3

Proof