ntrclsk3 - Mathbox for Richard Penner

	Mathbox for Richard Penner		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ntrclsk3		Structured version Visualization version GIF version

Theorem ntrclsk3 37388

Description: The intersection of interiors of a every pair is a subset of the interior of the intersection of the pair if an only if the closure of the union of every pair is a subset of the union of closures of the pair. (Contributed by RP, 19-Jun-2021.)

**Hypotheses**
Ref	Expression
ntrcls.o	⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
ntrcls.d	⊢ 𝐷 = (𝑂‘𝐵)
ntrcls.r	⊢ (𝜑 → 𝐼𝐷𝐾)

**Assertion**
Ref	Expression
ntrclsk3	⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Distinct variable groups: 𝐵,𝑠,𝑡,𝑖,𝑗,𝑘 𝐼,𝑠,𝑡,𝑖,𝑗,𝑘 𝜑,𝑠,𝑡,𝑖,𝑗,𝑘 Allowed substitution hints: 𝐷(𝑡,𝑖,𝑗,𝑘,𝑠) 𝐾(𝑡,𝑖,𝑗,𝑘,𝑠) 𝑂(𝑡,𝑖,𝑗,𝑘,𝑠)

Proof of Theorem ntrclsk3 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6103	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝐼‘𝑠) = (𝐼‘𝑎))
2	1	ineq1d 3775	. . . 4 ⊢ (𝑠 = 𝑎 → ((𝐼‘𝑠) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑡)))
3		ineq1 3769	. . . . 5 ⊢ (𝑠 = 𝑎 → (𝑠 ∩ 𝑡) = (𝑎 ∩ 𝑡))
4	3	fveq2d 6107	. . . 4 ⊢ (𝑠 = 𝑎 → (𝐼‘(𝑠 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑡)))
5	2, 4	sseq12d 3597	. . 3 ⊢ (𝑠 = 𝑎 → (((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡))))
6		fveq2 6103	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝐼‘𝑡) = (𝐼‘𝑏))
7	6	ineq2d 3776	. . . 4 ⊢ (𝑡 = 𝑏 → ((𝐼‘𝑎) ∩ (𝐼‘𝑡)) = ((𝐼‘𝑎) ∩ (𝐼‘𝑏)))
8		ineq2 3770	. . . . 5 ⊢ (𝑡 = 𝑏 → (𝑎 ∩ 𝑡) = (𝑎 ∩ 𝑏))
9	8	fveq2d 6107	. . . 4 ⊢ (𝑡 = 𝑏 → (𝐼‘(𝑎 ∩ 𝑡)) = (𝐼‘(𝑎 ∩ 𝑏)))
10	7, 9	sseq12d 3597	. . 3 ⊢ (𝑡 = 𝑏 → (((𝐼‘𝑎) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑎 ∩ 𝑡)) ↔ ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏))))
11	5, 10	cbvral2v 3155	. 2 ⊢ (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)))
12		ntrcls.d	. . . . . 6 ⊢ 𝐷 = (𝑂‘𝐵)
13		ntrcls.r	. . . . . 6 ⊢ (𝜑 → 𝐼𝐷𝐾)
14	12, 13	ntrclsbex 37352	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ V)
15		difssd 3700	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ⊆ 𝐵)
16	14, 15	sselpwd 4734	. . . 4 ⊢ (𝜑 → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
17	16	adantr 480	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
18		elpwi 4117	. . . 4 ⊢ (𝑎 ∈ 𝒫 𝐵 → 𝑎 ⊆ 𝐵)
19		simpl 472	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → 𝐵 ∈ V)
20		difssd 3700	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ⊆ 𝐵)
21	19, 20	sselpwd 4734	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ 𝑎) ∈ 𝒫 𝐵)
22		simpr 476	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → 𝑠 = (𝐵 ∖ 𝑎))
23	22	difeq2d 3690	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝐵 ∖ 𝑠) = (𝐵 ∖ (𝐵 ∖ 𝑎)))
24	23	eqeq2d 2620	. . . . . 6 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ 𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎))))
25		eqcom 2617	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ (𝐵 ∖ 𝑎)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
26	24, 25	syl6bb 275	. . . . 5 ⊢ (((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) ∧ 𝑠 = (𝐵 ∖ 𝑎)) → (𝑎 = (𝐵 ∖ 𝑠) ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎))
27		dfss4 3820	. . . . . . 7 ⊢ (𝑎 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
28	27	biimpi 205	. . . . . 6 ⊢ (𝑎 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
29	28	adantl 481	. . . . 5 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑎)) = 𝑎)
30	21, 26, 29	rspcedvd 3289	. . . 4 ⊢ ((𝐵 ∈ V ∧ 𝑎 ⊆ 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
31	14, 18, 30	syl2an 493	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ 𝒫 𝐵) → ∃𝑠 ∈ 𝒫 𝐵𝑎 = (𝐵 ∖ 𝑠))
32		simpl1 1057	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → 𝜑)
33		difssd 3700	. . . . . 6 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ⊆ 𝐵)
34	14, 33	sselpwd 4734	. . . . 5 ⊢ (𝜑 → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
35	32, 34	syl 17	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵) → (𝐵 ∖ 𝑡) ∈ 𝒫 𝐵)
36		elpwi 4117	. . . . . 6 ⊢ (𝑏 ∈ 𝒫 𝐵 → 𝑏 ⊆ 𝐵)
37		simpl 472	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → 𝐵 ∈ V)
38		difssd 3700	. . . . . . . 8 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ⊆ 𝐵)
39	37, 38	sselpwd 4734	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ 𝑏) ∈ 𝒫 𝐵)
40		simpr 476	. . . . . . . . . 10 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → 𝑡 = (𝐵 ∖ 𝑏))
41	40	difeq2d 3690	. . . . . . . . 9 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝐵 ∖ 𝑡) = (𝐵 ∖ (𝐵 ∖ 𝑏)))
42	41	eqeq2d 2620	. . . . . . . 8 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ 𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏))))
43		eqcom 2617	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ (𝐵 ∖ 𝑏)) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
44	42, 43	syl6bb 275	. . . . . . 7 ⊢ (((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) ∧ 𝑡 = (𝐵 ∖ 𝑏)) → (𝑏 = (𝐵 ∖ 𝑡) ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏))
45		dfss4 3820	. . . . . . . . 9 ⊢ (𝑏 ⊆ 𝐵 ↔ (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
46	45	biimpi 205	. . . . . . . 8 ⊢ (𝑏 ⊆ 𝐵 → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
47	46	adantl 481	. . . . . . 7 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → (𝐵 ∖ (𝐵 ∖ 𝑏)) = 𝑏)
48	39, 44, 47	rspcedvd 3289	. . . . . 6 ⊢ ((𝐵 ∈ V ∧ 𝑏 ⊆ 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
49	14, 36, 48	syl2an 493	. . . . 5 ⊢ ((𝜑 ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
50	49	3ad2antl1 1216	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑏 ∈ 𝒫 𝐵) → ∃𝑡 ∈ 𝒫 𝐵𝑏 = (𝐵 ∖ 𝑡))
51		simp13 1086	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑎 = (𝐵 ∖ 𝑠))
52		fveq2 6103	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘𝑎) = (𝐼‘(𝐵 ∖ 𝑠)))
53	52	ineq1d 3775	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → ((𝐼‘𝑎) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)))
54		ineq1 3769	. . . . . . . 8 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝑎 ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ 𝑏))
55	54	fveq2d 6107	. . . . . . 7 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (𝐼‘(𝑎 ∩ 𝑏)) = (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)))
56	53, 55	sseq12d 3597	. . . . . 6 ⊢ (𝑎 = (𝐵 ∖ 𝑠) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
57	51, 56	syl 17	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏))))
58		fveq2 6103	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘𝑏) = (𝐼‘(𝐵 ∖ 𝑡)))
59	58	ineq2d 3776	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) = ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))
60		ineq2 3770	. . . . . . . . 9 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡)))
61		difundi 3838	. . . . . . . . 9 ⊢ (𝐵 ∖ (𝑠 ∪ 𝑡)) = ((𝐵 ∖ 𝑠) ∩ (𝐵 ∖ 𝑡))
62	60, 61	syl6eqr 2662	. . . . . . . 8 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → ((𝐵 ∖ 𝑠) ∩ 𝑏) = (𝐵 ∖ (𝑠 ∪ 𝑡)))
63	62	fveq2d 6107	. . . . . . 7 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) = (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))))
64	59, 63	sseq12d 3597	. . . . . 6 ⊢ (𝑏 = (𝐵 ∖ 𝑡) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
65	64	3ad2ant3 1077	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘((𝐵 ∖ 𝑠) ∩ 𝑏)) ↔ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
66		simp11 1084	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝜑)
67		ntrcls.o	. . . . . . . . . 10 ⊢ 𝑂 = (𝑖 ∈ V ↦ (𝑘 ∈ (𝒫 𝑖 ↑_𝑚 𝒫 𝑖) ↦ (𝑗 ∈ 𝒫 𝑖 ↦ (𝑖 ∖ (𝑘‘(𝑖 ∖ 𝑗))))))
68	67, 12, 13	ntrclsiex 37371	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵))
69	68, 14	jca 553	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V))
70	66, 69	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V))
71		elmapi 7765	. . . . . . . . . . . 12 ⊢ (𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
72	71	adantr 480	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐼:𝒫 𝐵⟶𝒫 𝐵)
73		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → 𝐵 ∈ V)
74		difssd 3700	. . . . . . . . . . . 12 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ⊆ 𝐵)
75	73, 74	sselpwd 4734	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ 𝑠) ∈ 𝒫 𝐵)
76	72, 75	ffvelrnd 6268	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ∈ 𝒫 𝐵)
77	76	elpwid 4118	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵)
78		orc 399	. . . . . . . . 9 ⊢ ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 → ((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵))
79		inss 3804	. . . . . . . . 9 ⊢ (((𝐼‘(𝐵 ∖ 𝑠)) ⊆ 𝐵 ∨ (𝐼‘(𝐵 ∖ 𝑡)) ⊆ 𝐵) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
80	77, 78, 79	3syl 18	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵)
81		difssd 3700	. . . . . . . . . . 11 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ⊆ 𝐵)
82	73, 81	sselpwd 4734	. . . . . . . . . 10 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐵 ∖ (𝑠 ∪ 𝑡)) ∈ 𝒫 𝐵)
83	72, 82	ffvelrnd 6268	. . . . . . . . 9 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ∈ 𝒫 𝐵)
84	83	elpwid 4118	. . . . . . . 8 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵)
85	80, 84	jca 553	. . . . . . 7 ⊢ ((𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵) ∧ 𝐵 ∈ V) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵))
86		sscon34b 37337	. . . . . . 7 ⊢ ((((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ 𝐵 ∧ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ⊆ 𝐵) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
87	70, 85, 86	3syl 18	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))))))
88		difindi 3840	. . . . . . . 8 ⊢ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
89	88	sseq2i 3593	. . . . . . 7 ⊢ ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))))
90	89	a1i 11	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ (𝐵 ∖ ((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))))
91	66, 14	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐵 ∈ V)
92	66, 68	syl 17	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵))
93		simp12 1085	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑠 ∈ 𝒫 𝐵)
94		rp-simp2 37107	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → 𝑡 ∈ 𝒫 𝐵)
95		simpl2 1058	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
96		simpl3 1059	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵))
97		eqid 2610	. . . . . . . . . 10 ⊢ (𝐷‘𝐼) = (𝐷‘𝐼)
98		simpl 472	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝐵 ∈ V)
99		simprl 790	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
100	99	elpwid 4118	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ⊆ 𝐵)
101		simprr 792	. . . . . . . . . . . . . 14 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
102	101	elpwid 4118	. . . . . . . . . . . . 13 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ⊆ 𝐵)
103	100, 102	unssd 3751	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ⊆ 𝐵)
104	98, 103	sselpwd 4734	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ V ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
105	104	3ad2antl2 1217	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝑠 ∪ 𝑡) ∈ 𝒫 𝐵)
106		eqid 2610	. . . . . . . . . 10 ⊢ ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡))
107	67, 12, 95, 96, 97, 105, 106	dssmapfv3d 37333	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))))
108		simpl1 1057	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝜑)
109	67, 12, 13	ntrclsfv1 37373	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐷‘𝐼) = 𝐾)
110	109	fveq1d 6105	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
111	108, 110	syl 17	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘(𝑠 ∪ 𝑡)) = (𝐾‘(𝑠 ∪ 𝑡)))
112	107, 111	eqtr3d 2646	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) = (𝐾‘(𝑠 ∪ 𝑡)))
113		simprl 790	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑠 ∈ 𝒫 𝐵)
114		eqid 2610	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑠) = ((𝐷‘𝐼)‘𝑠)
115	67, 12, 95, 96, 97, 113, 114	dssmapfv3d 37333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))))
116	109	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
117	108, 116	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑠) = (𝐾‘𝑠))
118	115, 117	eqtr3d 2646	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) = (𝐾‘𝑠))
119		simprr 792	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → 𝑡 ∈ 𝒫 𝐵)
120		eqid 2610	. . . . . . . . . . 11 ⊢ ((𝐷‘𝐼)‘𝑡) = ((𝐷‘𝐼)‘𝑡)
121	67, 12, 95, 96, 97, 119, 120	dssmapfv3d 37333	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))))
122	109	fveq1d 6105	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
123	108, 122	syl 17	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐷‘𝐼)‘𝑡) = (𝐾‘𝑡))
124	121, 123	eqtr3d 2646	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡))) = (𝐾‘𝑡))
125	118, 124	uneq12d 3730	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) = ((𝐾‘𝑠) ∪ (𝐾‘𝑡)))
126	112, 125	sseq12d 3597	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐵 ∈ V ∧ 𝐼 ∈ (𝒫 𝐵 ↑_𝑚 𝒫 𝐵)) ∧ (𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 ∈ 𝒫 𝐵)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
127	66, 91, 92, 93, 94, 126	syl32anc 1326	. . . . . 6 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → ((𝐵 ∖ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡)))) ⊆ ((𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑠))) ∪ (𝐵 ∖ (𝐼‘(𝐵 ∖ 𝑡)))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
128	87, 90, 127	3bitrd 293	. . . . 5 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘(𝐵 ∖ 𝑠)) ∩ (𝐼‘(𝐵 ∖ 𝑡))) ⊆ (𝐼‘(𝐵 ∖ (𝑠 ∪ 𝑡))) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
129	57, 65, 128	3bitrd 293	. . . 4 ⊢ (((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) ∧ 𝑡 ∈ 𝒫 𝐵 ∧ 𝑏 = (𝐵 ∖ 𝑡)) → (((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ (𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
130	35, 50, 129	ralxfrd2 4810	. . 3 ⊢ ((𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑎 = (𝐵 ∖ 𝑠)) → (∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
131	17, 31, 130	ralxfrd2 4810	. 2 ⊢ (𝜑 → (∀𝑎 ∈ 𝒫 𝐵∀𝑏 ∈ 𝒫 𝐵((𝐼‘𝑎) ∩ (𝐼‘𝑏)) ⊆ (𝐼‘(𝑎 ∩ 𝑏)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))
132	11, 131	syl5bb 271	1 ⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝐼‘𝑠) ∩ (𝐼‘𝑡)) ⊆ (𝐼‘(𝑠 ∩ 𝑡)) ↔ ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵(𝐾‘(𝑠 ∪ 𝑡)) ⊆ ((𝐾‘𝑠) ∪ (𝐾‘𝑡))))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∀wral 2896 ∃wrex 2897 Vcvv 3173 ∖ cdif 3537 ∪ cun 3538 ∩ cin 3539 ⊆ wss 3540 𝒫 cpw 4108 class class class wbr 4583 ↦ cmpt 4643 ⟶wf 5800 ‘cfv 5804 (class class class)co 6549 ↑_𝑚 cmap 7744

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-rep 4699 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847 ax-frege1 37104

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ne 2782 df-ral 2901 df-rex 2902 df-reu 2903 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-pw 4110 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-iun 4457 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-res 5050 df-ima 5051 df-iota 5768 df-fun 5806 df-fn 5807 df-f 5808 df-f1 5809 df-fo 5810 df-f1o 5811 df-fv 5812 df-ov 6552 df-oprab 6553 df-mpt2 6554 df-1st 7059 df-2nd 7060 df-map 7746

This theorem is referenced by: (None)

W3C validator