Metamath Proof Explorer

Theorem ordtuni

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

Ref Expression
Hypotheses ordtval.1 ⊢ X = dom ⁡ R
ordtval.2 ⊢ A = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x
ordtval.3 ⊢ B = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
Assertion ordtuni ⊢ R ∈ V → X = ⋃ X ∪ A ∪ B

Proof

Step Hyp Ref Expression
1 ordtval.1 ⊢ X = dom ⁡ R
2 ordtval.2 ⊢ A = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x
3 ordtval.3 ⊢ B = ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y
4 dmexg ⊢ R ∈ V → dom ⁡ R ∈ V
5 1 4 eqeltrid ⊢ R ∈ V → X ∈ V
6 unisng ⊢ X ∈ V → ⋃ X = X
7 5 6 syl ⊢ R ∈ V → ⋃ X = X
8 7 uneq1d ⊢ R ∈ V → ⋃ X ∪ ⋃ A ∪ B = X ∪ ⋃ A ∪ B
9 ssrab2 ⊢ y ∈ X | ¬ y R x ⊆ X
10 5 adantr ⊢ R ∈ V ∧ x ∈ X → X ∈ V
11 elpw2g ⊢ X ∈ V → y ∈ X | ¬ y R x ∈ 𝒫 X ↔ y ∈ X | ¬ y R x ⊆ X
12 10 11 syl ⊢ R ∈ V ∧ x ∈ X → y ∈ X | ¬ y R x ∈ 𝒫 X ↔ y ∈ X | ¬ y R x ⊆ X
13 9 12 mpbiri ⊢ R ∈ V ∧ x ∈ X → y ∈ X | ¬ y R x ∈ 𝒫 X
14 13 fmpttd ⊢ R ∈ V → x ∈ X ⟼ y ∈ X | ¬ y R x : X ⟶ 𝒫 X
15 14 frnd ⊢ R ∈ V → ran ⁡ x ∈ X ⟼ y ∈ X | ¬ y R x ⊆ 𝒫 X
16 2 15 eqsstrid ⊢ R ∈ V → A ⊆ 𝒫 X
17 ssrab2 ⊢ y ∈ X | ¬ x R y ⊆ X
18 elpw2g ⊢ X ∈ V → y ∈ X | ¬ x R y ∈ 𝒫 X ↔ y ∈ X | ¬ x R y ⊆ X
19 10 18 syl ⊢ R ∈ V ∧ x ∈ X → y ∈ X | ¬ x R y ∈ 𝒫 X ↔ y ∈ X | ¬ x R y ⊆ X
20 17 19 mpbiri ⊢ R ∈ V ∧ x ∈ X → y ∈ X | ¬ x R y ∈ 𝒫 X
21 20 fmpttd ⊢ R ∈ V → x ∈ X ⟼ y ∈ X | ¬ x R y : X ⟶ 𝒫 X
22 21 frnd ⊢ R ∈ V → ran ⁡ x ∈ X ⟼ y ∈ X | ¬ x R y ⊆ 𝒫 X
23 3 22 eqsstrid ⊢ R ∈ V → B ⊆ 𝒫 X
24 16 23 unssd ⊢ R ∈ V → A ∪ B ⊆ 𝒫 X
25 sspwuni ⊢ A ∪ B ⊆ 𝒫 X ↔ ⋃ A ∪ B ⊆ X
26 24 25 sylib ⊢ R ∈ V → ⋃ A ∪ B ⊆ X
27 ssequn2 ⊢ ⋃ A ∪ B ⊆ X ↔ X ∪ ⋃ A ∪ B = X
28 26 27 sylib ⊢ R ∈ V → X ∪ ⋃ A ∪ B = X
29 8 28 eqtr2d ⊢ R ∈ V → X = ⋃ X ∪ ⋃ A ∪ B
30 uniun ⊢ ⋃ X ∪ A ∪ B = ⋃ X ∪ ⋃ A ∪ B
31 29 30 eqtr4di ⊢ R ∈ V → X = ⋃ X ∪ A ∪ B