Theorem ntrneix13

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

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneix13	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		dfss3	⊢ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) )
5	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8	6 7	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	1 2 3	ntrneibex	⊢ ( 𝜑 → 𝐵 ∈ V )
10	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
11		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
12	11	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ⊆ 𝐵 )
13		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
14	13	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 ⊆ 𝐵 )
15	12 14	unssd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
16	10 15	sselpwd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
17	8 16	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ∈ 𝒫 𝐵 )
18	17	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 )
19		ralss	⊢ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
20	18 19	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
21	4 20	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
22		dfss3	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) )
23	8 11	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
24	23	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
25	8 13	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑡 ) ∈ 𝒫 𝐵 )
26	25	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑡 ) ⊆ 𝐵 )
27	24 26	unssd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
28		ralss	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ) )
29	27 28	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ) )
30	22 29	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ) )
31	21 30	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ) ) )
32		eqss	⊢ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) )
33		ralbiim	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ) ) )
34	31 32 33	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ) )
35	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
36		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
37	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐵 ∈ V )
38		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
39	38	elpwid	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ⊆ 𝐵 )
40		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
41	40	elpwid	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ⊆ 𝐵 )
42	39 41	unssd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ⊆ 𝐵 )
43	37 42	sselpwd	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∪ 𝑡 ) ∈ 𝒫 𝐵 )
44	1 2 35 36 43	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
45		elun	⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
46	1 2 35 36 38	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
47	1 2 35 36 40	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
48	46 47	orbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∨ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
49	45 48	syl5bb	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
50	44 49	bibi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
51	50	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
52	34 51	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
53	52	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
54		ralcom	⊢ ( ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
55	53 54	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
56	55	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
57		ralcom	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
58	56 57	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∪ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∪ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∪ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∨ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )