Theorem ordtt1

Description: The order topology is T_1 for any poset. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	ordtt1	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Fre )

Proof

Step	Hyp	Ref	Expression
1		ordttop	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Top )
2		snssi	⊢ ( 𝑥 ∈ dom 𝑅 → { 𝑥 } ⊆ dom 𝑅 )
3	2	adantl	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } ⊆ dom 𝑅 )
4		sseqin2	⊢ ( { 𝑥 } ⊆ dom 𝑅 ↔ ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑥 } )
5	3 4	sylib	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑥 } )
6		velsn	⊢ ( 𝑦 ∈ { 𝑥 } ↔ 𝑦 = 𝑥 )
7		eqid	⊢ dom 𝑅 = dom 𝑅
8	7	psref	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
9	8	adantr	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → 𝑥 𝑅 𝑥 )
10	9 9	jca	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑥 𝑅 𝑥 ∧ 𝑥 𝑅 𝑥 ) )
11		breq2	⊢ ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ↔ 𝑥 𝑅 𝑥 ) )
12		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 𝑅 𝑥 ↔ 𝑥 𝑅 𝑥 ) )
13	11 12	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑥 ∧ 𝑥 𝑅 𝑥 ) ) )
14	10 13	syl5ibrcom	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 = 𝑥 → ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
15		psasym	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑥 = 𝑦 )
16	15	equcomd	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 )
17	16	3expib	⊢ ( 𝑅 ∈ PosetRel → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 ) )
18	17	ad2antrr	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) → 𝑦 = 𝑥 ) )
19	14 18	impbid	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 = 𝑥 ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
20	6 19	syl5bb	⊢ ( ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) ∧ 𝑦 ∈ dom 𝑅 ) → ( 𝑦 ∈ { 𝑥 } ↔ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) ) )
21	20	rabbi2dva	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → ( dom 𝑅 ∩ { 𝑥 } ) = { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } )
22	5 21	eqtr3d	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } = { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } )
23	7	ordtcld3	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
24	23	3anidm23	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑦 ∈ dom 𝑅 ∣ ( 𝑥 𝑅 𝑦 ∧ 𝑦 𝑅 𝑥 ) } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
25	22 24	eqeltrd	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝑥 ∈ dom 𝑅 ) → { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
26	25	ralrimiva	⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ dom 𝑅 { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
27	7	ordttopon	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) )
28		toponuni	⊢ ( ( ordTop ‘ 𝑅 ) ∈ ( TopOn ‘ dom 𝑅 ) → dom 𝑅 = ∪ ( ordTop ‘ 𝑅 ) )
29	27 28	syl	⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ∪ ( ordTop ‘ 𝑅 ) )
30	29	raleqdv	⊢ ( 𝑅 ∈ PosetRel → ( ∀ 𝑥 ∈ dom 𝑅 { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ↔ ∀ 𝑥 ∈ ∪ ( ordTop ‘ 𝑅 ) { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ) )
31	26 30	mpbid	⊢ ( 𝑅 ∈ PosetRel → ∀ 𝑥 ∈ ∪ ( ordTop ‘ 𝑅 ) { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) )
32		eqid	⊢ ∪ ( ordTop ‘ 𝑅 ) = ∪ ( ordTop ‘ 𝑅 )
33	32	ist1	⊢ ( ( ordTop ‘ 𝑅 ) ∈ Fre ↔ ( ( ordTop ‘ 𝑅 ) ∈ Top ∧ ∀ 𝑥 ∈ ∪ ( ordTop ‘ 𝑅 ) { 𝑥 } ∈ ( Clsd ‘ ( ordTop ‘ 𝑅 ) ) ) )
34	1 31 33	sylanbrc	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) ∈ Fre )