ordtrest2

Description: An interval-closed set A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in RR , but in other sets like QQ there are interval-closed sets like ( _pi , +oo ) i^i QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015)

	Ref	Expression
Hypotheses	ordtrest2.1	⊢ 𝑋 = dom 𝑅
	ordtrest2.2	⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
	ordtrest2.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
	ordtrest2.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
Assertion	ordtrest2	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtrest2.1	⊢ 𝑋 = dom 𝑅
2		ordtrest2.2	⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
3		ordtrest2.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4		ordtrest2.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
5		tsrps	⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
6	2 5	syl	⊢ ( 𝜑 → 𝑅 ∈ PosetRel )
7	2	dmexd	⊢ ( 𝜑 → dom 𝑅 ∈ V )
8	1 7	eqeltrid	⊢ ( 𝜑 → 𝑋 ∈ V )
9	8 3	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
10		ordtrest	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ∈ V ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) )
11	6 9 10	syl2anc	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) )
12		eqid	⊢ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) = ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } )
13		eqid	⊢ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } )
14	1 12 13	ordtval	⊢ ( 𝑅 ∈ TosetRel → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) )
15	2 14	syl	⊢ ( 𝜑 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) )
16	15	oveq1d	⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
17		fibas	⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ∈ TopBases
18		tgrest	⊢ ( ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ∈ TopBases ∧ 𝐴 ∈ V ) → ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
19	17 9 18	sylancr	⊢ ( 𝜑 → ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
20	16 19	eqtr4d	⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) = ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) )
21		firest	⊢ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ) = ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾_t 𝐴 )
22	21	fveq2i	⊢ ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) = ( topGen ‘ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ) ↾_t 𝐴 ) )
23	20 22	eqtr4di	⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) = ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) )
24		inex1g	⊢ ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
25	2 24	syl	⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
26		ordttop	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
27	25 26	syl	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
28	1 12 13	ordtuni	⊢ ( 𝑅 ∈ TosetRel → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) )
29	2 28	syl	⊢ ( 𝜑 → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) )
30	29 8	eqeltrrd	⊢ ( 𝜑 → ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
31		uniexb	⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
32	30 31	sylibr	⊢ ( 𝜑 → ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V )
33		restval	⊢ ( ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ∈ V ∧ 𝐴 ∈ V ) → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
34	32 9 33	syl2anc	⊢ ( 𝜑 → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
35		sseqin2	⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
36	3 35	sylib	⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
37		eqid	⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) )
38	37	ordttopon	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
39	25 38	syl	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
40	1	psssdm	⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
41	6 3 40	syl2anc	⊢ ( 𝜑 → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
42	41	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( TopOn ‘ 𝐴 ) )
43	39 42	eleqtrd	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) )
44		toponmax	⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
45	43 44	syl	⊢ ( 𝜑 → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
46	36 45	eqeltrd	⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
47		elsni	⊢ ( 𝑣 ∈ { 𝑋 } → 𝑣 = 𝑋 )
48	47	ineq1d	⊢ ( 𝑣 ∈ { 𝑋 } → ( 𝑣 ∩ 𝐴 ) = ( 𝑋 ∩ 𝐴 ) )
49	48	eleq1d	⊢ ( 𝑣 ∈ { 𝑋 } → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑋 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
50	46 49	syl5ibrcom	⊢ ( 𝜑 → ( 𝑣 ∈ { 𝑋 } → ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
51	50	ralrimiv	⊢ ( 𝜑 → ∀ 𝑣 ∈ { 𝑋 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
52	1 2 3 4	ordtrest2lem	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
53		df-rn	⊢ ran 𝑅 = dom ^◡ 𝑅
54		cnvtsr	⊢ ( 𝑅 ∈ TosetRel → ^◡ 𝑅 ∈ TosetRel )
55	2 54	syl	⊢ ( 𝜑 → ^◡ 𝑅 ∈ TosetRel )
56	1	psrn	⊢ ( 𝑅 ∈ PosetRel → 𝑋 = ran 𝑅 )
57	6 56	syl	⊢ ( 𝜑 → 𝑋 = ran 𝑅 )
58	3 57	sseqtrd	⊢ ( 𝜑 → 𝐴 ⊆ ran 𝑅 )
59	57	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑋 = ran 𝑅 )
60	59	rabeqdv	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } )
61		vex	⊢ 𝑦 ∈ V
62		vex	⊢ 𝑧 ∈ V
63	61 62	brcnv	⊢ ( 𝑦 ^◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑦 )
64		vex	⊢ 𝑥 ∈ V
65	62 64	brcnv	⊢ ( 𝑧 ^◡ 𝑅 𝑥 ↔ 𝑥 𝑅 𝑧 )
66	63 65	anbi12ci	⊢ ( ( 𝑦 ^◡ 𝑅 𝑧 ∧ 𝑧 ^◡ 𝑅 𝑥 ) ↔ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) )
67	66	rabbii	⊢ { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ^◡ 𝑅 𝑧 ∧ 𝑧 ^◡ 𝑅 𝑥 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) }
68	60 67	eqtr4di	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } = { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ^◡ 𝑅 𝑧 ∧ 𝑧 ^◡ 𝑅 𝑥 ) } )
69	68 4	eqsstrrd	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ^◡ 𝑅 𝑧 ∧ 𝑧 ^◡ 𝑅 𝑥 ) } ⊆ 𝐴 )
70	69	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → { 𝑧 ∈ ran 𝑅 ∣ ( 𝑦 ^◡ 𝑅 𝑧 ∧ 𝑧 ^◡ 𝑅 𝑥 ) } ⊆ 𝐴 )
71	53 55 58 70	ordtrest2lem	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ^◡ 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
72		vex	⊢ 𝑤 ∈ V
73	72 62	brcnv	⊢ ( 𝑤 ^◡ 𝑅 𝑧 ↔ 𝑧 𝑅 𝑤 )
74	73	bicomi	⊢ ( 𝑧 𝑅 𝑤 ↔ 𝑤 ^◡ 𝑅 𝑧 )
75	74	a1i	⊢ ( 𝜑 → ( 𝑧 𝑅 𝑤 ↔ 𝑤 ^◡ 𝑅 𝑧 ) )
76	75	notbid	⊢ ( 𝜑 → ( ¬ 𝑧 𝑅 𝑤 ↔ ¬ 𝑤 ^◡ 𝑅 𝑧 ) )
77	57 76	rabeqbidv	⊢ ( 𝜑 → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } = { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ^◡ 𝑅 𝑧 } )
78	57 77	mpteq12dv	⊢ ( 𝜑 → ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ^◡ 𝑅 𝑧 } ) )
79	78	rneqd	⊢ ( 𝜑 → ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) = ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ^◡ 𝑅 𝑧 } ) )
80		cnvin	⊢ ^◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ^◡ 𝑅 ∩ ^◡ ( 𝐴 × 𝐴 ) )
81		cnvxp	⊢ ^◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 )
82	81	ineq2i	⊢ ( ^◡ 𝑅 ∩ ^◡ ( 𝐴 × 𝐴 ) ) = ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) )
83	80 82	eqtri	⊢ ^◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) )
84	83	fveq2i	⊢ ( ordTop ‘ ^◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
85		psss	⊢ ( 𝑅 ∈ PosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )
86	6 85	syl	⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel )
87		ordtcnv	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ PosetRel → ( ordTop ‘ ^◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
88	86 87	syl	⊢ ( 𝜑 → ( ordTop ‘ ^◡ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
89	84 88	syl5reqr	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
90	89	eleq2d	⊢ ( 𝜑 → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
91	79 90	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑣 ∈ ran ( 𝑧 ∈ ran 𝑅 ↦ { 𝑤 ∈ ran 𝑅 ∣ ¬ 𝑤 ^◡ 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
92	71 91	mpbird	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
93		ralunb	⊢ ( ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
94	52 92 93	sylanbrc	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
95		ralunb	⊢ ( ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ { 𝑋 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
96	51 94 95	sylanbrc	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
97		eqid	⊢ ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) = ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) )
98	97	fmpt	⊢ ( ∀ 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
99	96 98	sylib	⊢ ( 𝜑 → ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
100	99	frnd	⊢ ( 𝜑 → ran ( 𝑣 ∈ ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
101	34 100	eqsstrd	⊢ ( 𝜑 → ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
102		tgfiss	⊢ ( ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ∧ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) → ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
103	27 101 102	syl2anc	⊢ ( 𝜑 → ( topGen ‘ ( fi ‘ ( ( { 𝑋 } ∪ ( ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑧 𝑅 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
104	23 103	eqsstrd	⊢ ( 𝜑 → ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
105	11 104	eqssd	⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ 𝑅 ) ↾_t 𝐴 ) )

Metamath Proof Explorer

Theorem ordtrest2

Proof