Metamath Proof Explorer

Theorem ordtopn2

Description: A downward ray ( -oo , P ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Hypothesis ordttopon.3 ⊢ 𝑋 = dom 𝑅
Assertion ordtopn2 ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 ordttopon.3 ⊢ 𝑋 = dom 𝑅
2 eqid ⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) = ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } )
3 eqid ⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
4 1 2 3 ordtuni ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
5 4 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑋 = ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
6 dmexg ⊢ ( 𝑅 ∈ 𝑉 → dom 𝑅 ∈ V )
7 1 6 eqeltrid ⊢ ( 𝑅 ∈ 𝑉 → 𝑋 ∈ V )
8 7 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑋 ∈ V )
9 5 8 eqeltrrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
10 uniexb ⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V ↔ ∪ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
11 9 10 sylibr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V )
12 ssfii ⊢ ( ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ∈ V → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
13 11 12 syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
14 fibas ⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases
15 bastg ⊢ ( ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ∈ TopBases → ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
16 14 15 ax-mp ⊢ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) )
17 13 16 sstrdi ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
18 1 2 3 ordtval ⊢ ( 𝑅 ∈ 𝑉 → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
19 18 adantr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( ordTop ‘ 𝑅 ) = ( topGen ‘ ( fi ‘ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ) ) )
20 17 19 sseqtrrd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) ⊆ ( ordTop ‘ 𝑅 ) )
21 ssun2 ⊢ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ⊆ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
22 ssun2 ⊢ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ⊆ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
23 simpr ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
24 eqidd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } )
25 breq1 ⊢ ( 𝑦 = 𝑃 → ( 𝑦 𝑅 𝑥 ↔ 𝑃 𝑅 𝑥 ) )
26 25 notbid ⊢ ( 𝑦 = 𝑃 → ( ¬ 𝑦 𝑅 𝑥 ↔ ¬ 𝑃 𝑅 𝑥 ) )
27 26 rabbidv ⊢ ( 𝑦 = 𝑃 → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } )
28 27 rspceeqv ⊢ ( ( 𝑃 ∈ 𝑋 ∧ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ) → ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
29 23 24 28 syl2anc ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
30 rabexg ⊢ ( 𝑋 ∈ V → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ V )
31 eqid ⊢ ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) = ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } )
32 31 elrnmpt ⊢ ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ V → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
33 8 30 32 3syl ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → ( { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ↔ ∃ 𝑦 ∈ 𝑋 { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } = { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
34 29 33 mpbird ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) )
35 22 34 sseldi ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) )
36 21 35 sseldi ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ( { 𝑋 } ∪ ( ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑥 𝑅 𝑦 } ) ∪ ran ( 𝑦 ∈ 𝑋 ↦ { 𝑥 ∈ 𝑋 ∣ ¬ 𝑦 𝑅 𝑥 } ) ) ) )
37 20 36 sseldd ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑃 ∈ 𝑋 ) → { 𝑥 ∈ 𝑋 ∣ ¬ 𝑃 𝑅 𝑥 } ∈ ( ordTop ‘ 𝑅 ) )