ordtrest2NEW

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) (Revised by Thierry Arnoux, 11-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
	ordtrest2NEW.2	⊢ ( 𝜑 → 𝐾 ∈ Toset )
	ordtrest2NEW.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
	ordtrest2NEW.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
Assertion	ordtrest2NEW	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3		ordtrest2NEW.2	⊢ ( 𝜑 → 𝐾 ∈ Toset )
4		ordtrest2NEW.3	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
5		ordtrest2NEW.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
6		tospos	⊢ ( 𝐾 ∈ Toset → 𝐾 ∈ Poset )
7		posprs	⊢ ( 𝐾 ∈ Poset → 𝐾 ∈ Proset )
8	3 6 7	3syl	⊢ ( 𝜑 → 𝐾 ∈ Proset )
9	1 2	ordtrestNEW	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) )
10	8 4 9	syl2anc	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ⊆ ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) )
11		eqid	⊢ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) = ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } )
12		eqid	⊢ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) = ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } )
13	1 2 11 12	ordtprsval	⊢ ( 𝐾 ∈ Proset → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ) )
14	8 13	syl	⊢ ( 𝜑 → ( ordTop ‘ ≤ ) = ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ) )
15	14	oveq1d	⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) = ( ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
16		fibas	⊢ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ∈ TopBases
17	1	fvexi	⊢ 𝐵 ∈ V
18	17	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
19	18 4	ssexd	⊢ ( 𝜑 → 𝐴 ∈ V )
20		tgrest	⊢ ( ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ∈ TopBases ∧ 𝐴 ∈ V ) → ( topGen ‘ ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
21	16 19 20	sylancr	⊢ ( 𝜑 → ( topGen ‘ ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) = ( ( topGen ‘ ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ) ↾_t 𝐴 ) )
22	15 21	eqtr4d	⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) = ( topGen ‘ ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ↾_t 𝐴 ) ) )
23		firest	⊢ ( fi ‘ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ) = ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ↾_t 𝐴 )
24	23	fveq2i	⊢ ( topGen ‘ ( fi ‘ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) = ( topGen ‘ ( ( fi ‘ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ) ↾_t 𝐴 ) )
25	22 24	eqtr4di	⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) = ( topGen ‘ ( fi ‘ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) )
26		fvex	⊢ ( le ‘ 𝐾 ) ∈ V
27	26	inex1	⊢ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∈ V
28	2 27	eqeltri	⊢ ≤ ∈ V
29	28	inex1	⊢ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ V
30		ordttop	⊢ ( ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
31	29 30	mp1i	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
32	1 2 11 12	ordtprsuni	⊢ ( 𝐾 ∈ Proset → 𝐵 = ∪ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) )
33	8 32	syl	⊢ ( 𝜑 → 𝐵 = ∪ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) )
34	33 18	eqeltrrd	⊢ ( 𝜑 → ∪ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ∈ V )
35		uniexb	⊢ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ∈ V ↔ ∪ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ∈ V )
36	34 35	sylibr	⊢ ( 𝜑 → ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ∈ V )
37		restval	⊢ ( ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ∈ V ∧ 𝐴 ∈ V ) → ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
38	36 19 37	syl2anc	⊢ ( 𝜑 → ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) = ran ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) )
39		sseqin2	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐵 ∩ 𝐴 ) = 𝐴 )
40	4 39	sylib	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) = 𝐴 )
41		eqid	⊢ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = dom ( ≤ ∩ ( 𝐴 × 𝐴 ) )
42	41	ordttopon	⊢ ( ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
43	29 42	mp1i	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
44	1 2	prsssdm	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
45	8 4 44	syl2anc	⊢ ( 𝜑 → dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
46	45	fveq2d	⊢ ( 𝜑 → ( TopOn ‘ dom ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( TopOn ‘ 𝐴 ) )
47	43 46	eleqtrd	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) )
48		toponmax	⊢ ( ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
49	47 48	syl	⊢ ( 𝜑 → 𝐴 ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
50	40 49	eqeltrd	⊢ ( 𝜑 → ( 𝐵 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
51		elsni	⊢ ( 𝑣 ∈ { 𝐵 } → 𝑣 = 𝐵 )
52	51	ineq1d	⊢ ( 𝑣 ∈ { 𝐵 } → ( 𝑣 ∩ 𝐴 ) = ( 𝐵 ∩ 𝐴 ) )
53	52	eleq1d	⊢ ( 𝑣 ∈ { 𝐵 } → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝐵 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
54	50 53	syl5ibrcom	⊢ ( 𝜑 → ( 𝑣 ∈ { 𝐵 } → ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
55	54	ralrimiv	⊢ ( 𝜑 → ∀ 𝑣 ∈ { 𝐵 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
56	1 2 3 4 5	ordtrest2NEWlem	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
57		eqid	⊢ ( ODual ‘ 𝐾 ) = ( ODual ‘ 𝐾 )
58	57 1	odubas	⊢ 𝐵 = ( Base ‘ ( ODual ‘ 𝐾 ) )
59	2	cnveqi	⊢ ^◡ ≤ = ^◡ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
60		cnvin	⊢ ^◡ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) = ( ^◡ ( le ‘ 𝐾 ) ∩ ^◡ ( 𝐵 × 𝐵 ) )
61		cnvxp	⊢ ^◡ ( 𝐵 × 𝐵 ) = ( 𝐵 × 𝐵 )
62	61	ineq2i	⊢ ( ^◡ ( le ‘ 𝐾 ) ∩ ^◡ ( 𝐵 × 𝐵 ) ) = ( ^◡ ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
63		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
64	57 63	oduleval	⊢ ^◡ ( le ‘ 𝐾 ) = ( le ‘ ( ODual ‘ 𝐾 ) )
65	64	ineq1i	⊢ ( ^◡ ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) = ( ( le ‘ ( ODual ‘ 𝐾 ) ) ∩ ( 𝐵 × 𝐵 ) )
66	60 62 65	3eqtri	⊢ ^◡ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) = ( ( le ‘ ( ODual ‘ 𝐾 ) ) ∩ ( 𝐵 × 𝐵 ) )
67	59 66	eqtri	⊢ ^◡ ≤ = ( ( le ‘ ( ODual ‘ 𝐾 ) ) ∩ ( 𝐵 × 𝐵 ) )
68	57	odutos	⊢ ( 𝐾 ∈ Toset → ( ODual ‘ 𝐾 ) ∈ Toset )
69	3 68	syl	⊢ ( 𝜑 → ( ODual ‘ 𝐾 ) ∈ Toset )
70		vex	⊢ 𝑦 ∈ V
71		vex	⊢ 𝑧 ∈ V
72	70 71	brcnv	⊢ ( 𝑦 ^◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑦 )
73		vex	⊢ 𝑥 ∈ V
74	71 73	brcnv	⊢ ( 𝑧 ^◡ ≤ 𝑥 ↔ 𝑥 ≤ 𝑧 )
75	72 74	anbi12ci	⊢ ( ( 𝑦 ^◡ ≤ 𝑧 ∧ 𝑧 ^◡ ≤ 𝑥 ) ↔ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) )
76	75	rabbii	⊢ { 𝑧 ∈ 𝐵 ∣ ( 𝑦 ^◡ ≤ 𝑧 ∧ 𝑧 ^◡ ≤ 𝑥 ) } = { 𝑧 ∈ 𝐵 ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) }
77	76 5	eqsstrid	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑦 ^◡ ≤ 𝑧 ∧ 𝑧 ^◡ ≤ 𝑥 ) } ⊆ 𝐴 )
78	77	ancom2s	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑦 ^◡ ≤ 𝑧 ∧ 𝑧 ^◡ ≤ 𝑥 ) } ⊆ 𝐴 )
79	58 67 69 4 78	ordtrest2NEWlem	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ^◡ ≤ 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
80		vex	⊢ 𝑤 ∈ V
81	80 71	brcnv	⊢ ( 𝑤 ^◡ ≤ 𝑧 ↔ 𝑧 ≤ 𝑤 )
82	81	bicomi	⊢ ( 𝑧 ≤ 𝑤 ↔ 𝑤 ^◡ ≤ 𝑧 )
83	82	a1i	⊢ ( 𝜑 → ( 𝑧 ≤ 𝑤 ↔ 𝑤 ^◡ ≤ 𝑧 ) )
84	83	notbid	⊢ ( 𝜑 → ( ¬ 𝑧 ≤ 𝑤 ↔ ¬ 𝑤 ^◡ ≤ 𝑧 ) )
85	84	rabbidv	⊢ ( 𝜑 → { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } = { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ^◡ ≤ 𝑧 } )
86	85	mpteq2dv	⊢ ( 𝜑 → ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) = ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ^◡ ≤ 𝑧 } ) )
87	86	rneqd	⊢ ( 𝜑 → ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) = ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ^◡ ≤ 𝑧 } ) )
88		cnvin	⊢ ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ^◡ ≤ ∩ ^◡ ( 𝐴 × 𝐴 ) )
89		cnvxp	⊢ ^◡ ( 𝐴 × 𝐴 ) = ( 𝐴 × 𝐴 )
90	89	ineq2i	⊢ ( ^◡ ≤ ∩ ^◡ ( 𝐴 × 𝐴 ) ) = ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) )
91	88 90	eqtri	⊢ ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) )
92	91	fveq2i	⊢ ( ordTop ‘ ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) )
93	1	ressprs	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( 𝐾 ↾_s 𝐴 ) ∈ Proset )
94	8 4 93	syl2anc	⊢ ( 𝜑 → ( 𝐾 ↾_s 𝐴 ) ∈ Proset )
95		eqid	⊢ ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) = ( Base ‘ ( 𝐾 ↾_s 𝐴 ) )
96		eqid	⊢ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) = ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) )
97	95 96	ordtcnvNEW	⊢ ( ( 𝐾 ↾_s 𝐴 ) ∈ Proset → ( ordTop ‘ ^◡ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) = ( ordTop ‘ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) )
98	94 97	syl	⊢ ( 𝜑 → ( ordTop ‘ ^◡ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) = ( ordTop ‘ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) )
99	1 2	prsss	⊢ ( ( 𝐾 ∈ Proset ∧ 𝐴 ⊆ 𝐵 ) → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
100	8 4 99	syl2anc	⊢ ( 𝜑 → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) )
101		eqid	⊢ ( 𝐾 ↾_s 𝐴 ) = ( 𝐾 ↾_s 𝐴 )
102	101 63	ressle	⊢ ( 𝐴 ∈ V → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) )
103	19 102	syl	⊢ ( 𝜑 → ( le ‘ 𝐾 ) = ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) )
104	101 1	ressbas2	⊢ ( 𝐴 ⊆ 𝐵 → 𝐴 = ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) )
105	4 104	syl	⊢ ( 𝜑 → 𝐴 = ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) )
106	105	sqxpeqd	⊢ ( 𝜑 → ( 𝐴 × 𝐴 ) = ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) )
107	103 106	ineq12d	⊢ ( 𝜑 → ( ( le ‘ 𝐾 ) ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) )
108	100 107	eqtrd	⊢ ( 𝜑 → ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) )
109	108	cnveqd	⊢ ( 𝜑 → ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) = ^◡ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) )
110	109	fveq2d	⊢ ( 𝜑 → ( ordTop ‘ ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ^◡ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) )
111	108	fveq2d	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ( le ‘ ( 𝐾 ↾_s 𝐴 ) ) ∩ ( ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) × ( Base ‘ ( 𝐾 ↾_s 𝐴 ) ) ) ) ) )
112	98 110 111	3eqtr4d	⊢ ( 𝜑 → ( ordTop ‘ ^◡ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
113	92 112	syl5reqr	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ordTop ‘ ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
114	113	eleq2d	⊢ ( 𝜑 → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
115	87 114	raleqbidv	⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ^◡ ≤ 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ^◡ ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
116	79 115	mpbird	⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
117		ralunb	⊢ ( ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
118	56 116 117	sylanbrc	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
119		ralunb	⊢ ( ∀ 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( ∀ 𝑣 ∈ { 𝐵 } ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∧ ∀ 𝑣 ∈ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) )
120	55 118 119	sylanbrc	⊢ ( 𝜑 → ∀ 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
121		eqid	⊢ ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) = ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) )
122	121	fmpt	⊢ ( ∀ 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
123	120 122	sylib	⊢ ( 𝜑 → ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) : ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ⟶ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
124	123	frnd	⊢ ( 𝜑 → ran ( 𝑣 ∈ ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↦ ( 𝑣 ∩ 𝐴 ) ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
125	38 124	eqsstrd	⊢ ( 𝜑 → ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
126		tgfiss	⊢ ( ( ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top ∧ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) ) → ( topGen ‘ ( fi ‘ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
127	31 125 126	syl2anc	⊢ ( 𝜑 → ( topGen ‘ ( fi ‘ ( ( { 𝐵 } ∪ ( ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ∪ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑧 ≤ 𝑤 } ) ) ) ↾_t 𝐴 ) ) ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
128	25 127	eqsstrd	⊢ ( 𝜑 → ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) ⊆ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )
129	10 128	eqssd	⊢ ( 𝜑 → ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) = ( ( ordTop ‘ ≤ ) ↾_t 𝐴 ) )

Metamath Proof Explorer

Theorem ordtrest2NEW

Proof