Metamath Proof Explorer

Theorem ordtuni

Description: Value of the order topology. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypotheses ordtval.1 ⊢ 𝑋 = dom 𝑅
ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
Assertion ordtuni ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ 𝑋 = dom 𝑅
2 ordtval.2 ⊢ 𝐴 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
3 ordtval.3 ⊢ 𝐵 = ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
4 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
5 1 4 eqeltrid ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 ∈ V )
6 unisng ⊢ ( 𝑋 ∈ V → ∪ { 𝑋 } = 𝑋 )
7 5 6 syl ⊢ ( 𝑅 ∈ 𝑉 → ∪ { 𝑋 } = 𝑋 )
8 7 uneq1d ⊢ ( 𝑅 ∈ 𝑉 → ( ∪ { 𝑋 } ∪ ∪ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑋 ∪ ∪ ( 𝐴 ∪ 𝐵 ) ) )
9 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋
10 5 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → 𝑋 ∈ V )
11 elpw2g ⊢ ( 𝑋 ∈ V → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋 ) )
12 10 11 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ⊆ 𝑋 ) )
13 9 12 mpbiri ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ∈ 𝒫 𝑋 )
14 13 fmpttd ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) : 𝑋 ⟶ 𝒫 𝑋 )
15 14 frnd ⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ⊆ 𝒫 𝑋 )
16 2 15 eqsstrid ⊢ ( 𝑅 ∈ 𝑉 → 𝐴 ⊆ 𝒫 𝑋 )
17 ssrab2 ⊢ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ⊆ 𝑋
18 elpw2g ⊢ ( 𝑋 ∈ V → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ⊆ 𝑋 ) )
19 10 18 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → ( { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ 𝒫 𝑋 ↔ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ⊆ 𝑋 ) )
20 17 19 mpbiri ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑥 ∈ 𝑋 ) → { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ∈ 𝒫 𝑋 )
21 20 fmpttd ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) : 𝑋 ⟶ 𝒫 𝑋 )
22 21 frnd ⊢ ( 𝑅 ∈ 𝑉 → ran ( 𝑥 ∈ 𝑋 ↦ { 𝑦 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ⊆ 𝒫 𝑋 )
23 3 22 eqsstrid ⊢ ( 𝑅 ∈ 𝑉 → 𝐵 ⊆ 𝒫 𝑋 )
24 16 23 unssd ⊢ ( 𝑅 ∈ 𝑉 → ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝑋 )
25 sspwuni ⊢ ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝒫 𝑋 ↔ ∪ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
26 24 25 sylib ⊢ ( 𝑅 ∈ 𝑉 → ∪ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 )
27 ssequn2 ⊢ ( ∪ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑋 ↔ ( 𝑋 ∪ ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝑋 )
28 26 27 sylib ⊢ ( 𝑅 ∈ 𝑉 → ( 𝑋 ∪ ∪ ( 𝐴 ∪ 𝐵 ) ) = 𝑋 )
29 8 28 eqtr2d ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ( ∪ { 𝑋 } ∪ ∪ ( 𝐴 ∪ 𝐵 ) ) )
30 uniun ⊢ ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) = ( ∪ { 𝑋 } ∪ ∪ ( 𝐴 ∪ 𝐵 ) )
31 29 30 eqtr4di ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( { 𝑋 } ∪ ( 𝐴 ∪ 𝐵 ) ) )