Theorem ordtcnv

Description: The order dual generates the same topology as the original order. (Contributed by Mario Carneiro, 3-Sep-2015)

	Ref	Expression
Assertion	ordtcnv	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( ordTop ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ dom 𝑅 = dom 𝑅
2	1	psrn	⊢ ( 𝑅 ∈ PosetRel → dom 𝑅 = ran 𝑅 )
3	2	eqcomd	⊢ ( 𝑅 ∈ PosetRel → ran 𝑅 = dom 𝑅 )
4	3	sneqd	⊢ ( 𝑅 ∈ PosetRel → { ran 𝑅 } = { dom 𝑅 } )
5		vex	⊢ 𝑦 ∈ V
6		vex	⊢ 𝑥 ∈ V
7	5 6	brcnv	⊢ ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 )
8	7	a1i	⊢ ( 𝑅 ∈ PosetRel → ( 𝑦 ◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑦 ) )
9	8	notbid	⊢ ( 𝑅 ∈ PosetRel → ( ¬ 𝑦 ◡ 𝑅 𝑥 ↔ ¬ 𝑥 𝑅 𝑦 ) )
10	3 9	rabeqbidv	⊢ ( 𝑅 ∈ PosetRel → { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } = { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } )
11	3 10	mpteq12dv	⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
12	11	rneqd	⊢ ( 𝑅 ∈ PosetRel → ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
13	6 5	brcnv	⊢ ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 )
14	13	a1i	⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ◡ 𝑅 𝑦 ↔ 𝑦 𝑅 𝑥 ) )
15	14	notbid	⊢ ( 𝑅 ∈ PosetRel → ( ¬ 𝑥 ◡ 𝑅 𝑦 ↔ ¬ 𝑦 𝑅 𝑥 ) )
16	3 15	rabeqbidv	⊢ ( 𝑅 ∈ PosetRel → { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } = { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } )
17	3 16	mpteq12dv	⊢ ( 𝑅 ∈ PosetRel → ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
18	17	rneqd	⊢ ( 𝑅 ∈ PosetRel → ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
19	12 18	uneq12d	⊢ ( 𝑅 ∈ PosetRel → ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
20		uncom	⊢ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) )
21	19 20	eqtrdi	⊢ ( 𝑅 ∈ PosetRel → ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) = ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) )
22	4 21	uneq12d	⊢ ( 𝑅 ∈ PosetRel → ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) = ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) )
23	22	fveq2d	⊢ ( 𝑅 ∈ PosetRel → ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) = ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) )
24	23	fveq2d	⊢ ( 𝑅 ∈ PosetRel → ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) = ( topGen ‘ ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
25		cnvps	⊢ ( 𝑅 ∈ PosetRel → ◡ 𝑅 ∈ PosetRel )
26		df-rn	⊢ ran 𝑅 = dom ◡ 𝑅
27		eqid	⊢ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } )
28		eqid	⊢ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) = ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } )
29	26 27 28	ordtval	⊢ ( ◡ 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) )
30	25 29	syl	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { ran 𝑅 } ∪ ( ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑦 ◡ 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ ran 𝑅 ↦ { 𝑦 ∈ ran 𝑅 ∣ ¬ 𝑥 ◡ 𝑅 𝑦 } ) ) ) ) ) )
31		eqid	⊢ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } )
32		eqid	⊢ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } )
33	1 31 32	ordtval	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { dom 𝑅 } ∪ ( ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑦 𝑅 𝑥 } ) ∪ ran ( 𝑥 ∈ dom 𝑅 ↦ { 𝑦 ∈ dom 𝑅 ∣ ¬ 𝑥 𝑅 𝑦 } ) ) ) ) ) )
34	24 30 33	3eqtr4d	⊢ ( 𝑅 ∈ PosetRel → ( ordTop ‘ ◡ 𝑅 ) = ( ordTop ‘ 𝑅 ) )