Theorem ordtprsuni

Description: Value of the order topology. (Contributed by Thierry Arnoux, 13-Sep-2018)

	Ref	Expression
Hypotheses	ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
	ordtposval.e	⊢ 𝐸 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
	ordtposval.f	⊢ 𝐹 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
Assertion	ordtprsuni	⊢ ( 𝐾 ∈ Proset → 𝐵 = ∪ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ordtNEW.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		ordtNEW.l	⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
3		ordtposval.e	⊢ 𝐸 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
4		ordtposval.f	⊢ 𝐹 = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
5	1 2	prsdm	⊢ ( 𝐾 ∈ Proset → dom ≤ = 𝐵 )
6	5	sneqd	⊢ ( 𝐾 ∈ Proset → { dom ≤ } = { 𝐵 } )
7		biidd	⊢ ( 𝐾 ∈ Proset → ( ¬ 𝑦 ≤ 𝑥 ↔ ¬ 𝑦 ≤ 𝑥 ) )
8	5 7	rabeqbidv	⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } )
9	5 8	mpteq12dv	⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
10	9	rneqd	⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) )
11		biidd	⊢ ( 𝐾 ∈ Proset → ( ¬ 𝑥 ≤ 𝑦 ↔ ¬ 𝑥 ≤ 𝑦 ) )
12	5 11	rabeqbidv	⊢ ( 𝐾 ∈ Proset → { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } = { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } )
13	5 12	mpteq12dv	⊢ ( 𝐾 ∈ Proset → ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
14	13	rneqd	⊢ ( 𝐾 ∈ Proset → ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
15	10 14	uneq12d	⊢ ( 𝐾 ∈ Proset → ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) )
16	6 15	uneq12d	⊢ ( 𝐾 ∈ Proset → ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) = ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
17	16	unieqd	⊢ ( 𝐾 ∈ Proset → ∪ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) = ∪ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
18		fvex	⊢ ( le ‘ 𝐾 ) ∈ V
19	18	inex1	⊢ ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) ) ∈ V
20	2 19	eqeltri	⊢ ≤ ∈ V
21		eqid	⊢ dom ≤ = dom ≤
22		eqid	⊢ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) = ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } )
23		eqid	⊢ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) = ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } )
24	21 22 23	ordtuni	⊢ ( ≤ ∈ V → dom ≤ = ∪ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
25	20 24	ax-mp	⊢ dom ≤ = ∪ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) )
26	5 25	eqtr3di	⊢ ( 𝐾 ∈ Proset → 𝐵 = ∪ ( { dom ≤ } ∪ ( ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ dom ≤ ↦ { 𝑦 ∈ dom ≤ ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
27	3 4	uneq12i	⊢ ( 𝐸 ∪ 𝐹 ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) )
28	27	a1i	⊢ ( 𝐾 ∈ Proset → ( 𝐸 ∪ 𝐹 ) = ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) )
29	28	uneq2d	⊢ ( 𝐾 ∈ Proset → ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) = ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
30	29	unieqd	⊢ ( 𝐾 ∈ Proset → ∪ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) = ∪ ( { 𝐵 } ∪ ( ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑦 ≤ 𝑥 } ) ∪ ran ( 𝑥 ∈ 𝐵 ↦ { 𝑦 ∈ 𝐵 ∣ ¬ 𝑥 ≤ 𝑦 } ) ) ) )
31	17 26 30	3eqtr4d	⊢ ( 𝐾 ∈ Proset → 𝐵 = ∪ ( { 𝐵 } ∪ ( 𝐸 ∪ 𝐹 ) ) )