Metamath Proof Explorer

Theorem ordtrest2lem

Description: Lemma for ordtrest2 . (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses ordtrest2.1 ⊢ 𝑋 = dom 𝑅
ordtrest2.2 ⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
ordtrest2.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
ordtrest2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
Assertion ordtrest2lem ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 ordtrest2.1 ⊢ 𝑋 = dom 𝑅
2 ordtrest2.2 ⊢ ( 𝜑 → 𝑅 ∈ TosetRel )
3 ordtrest2.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑋 )
4 ordtrest2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 )
5 inrab2 ⊢ ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) = { 𝑤 ∈ ( 𝑋 ∩ 𝐴 ) ∣ ¬ 𝑤 𝑅 𝑧 }
6 sseqin2 ⊢ ( 𝐴 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝐴 ) = 𝐴 )
7 3 6 sylib ⊢ ( 𝜑 → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
8 7 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑋 ∩ 𝐴 ) = 𝐴 )
9 8 rabeqdv ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → { 𝑤 ∈ ( 𝑋 ∩ 𝐴 ) ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } )
10 5 9 eqtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } )
11 inex1g ⊢ ( 𝑅 ∈ TosetRel → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
12 2 11 syl ⊢ ( 𝜑 → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
13 eqid ⊢ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) )
14 13 ordttopon ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
15 12 14 syl ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
16 tsrps ⊢ ( 𝑅 ∈ TosetRel → 𝑅 ∈ PosetRel )
17 2 16 syl ⊢ ( 𝜑 → 𝑅 ∈ PosetRel )
18 1 psssdm ⊢ ( ( 𝑅 ∈ PosetRel ∧ 𝐴 ⊆ 𝑋 ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
19 17 3 18 syl2anc ⊢ ( 𝜑 → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
20 19 fveq2d ⊢ ( 𝜑 → ( TopOn ‘ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) = ( TopOn ‘ 𝐴 ) )
21 15 20 eleqtrd ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) )
22 toponmax ⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ ( TopOn ‘ 𝐴 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
23 21 22 syl ⊢ ( 𝜑 → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
25 rabid2 ⊢ ( 𝐴 = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ↔ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 )
26 eleq1 ⊢ ( 𝐴 = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } → ( 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
27 25 26 sylbir ⊢ ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → ( 𝐴 ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
28 24 27 syl5ibcom ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
29 dfrex2 ⊢ ( ∃ 𝑤 ∈ 𝐴 𝑤 𝑅 𝑧 ↔ ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 )
30 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 𝑅 𝑧 ↔ 𝑥 𝑅 𝑧 ) )
31 30 cbvrexvw ⊢ ( ∃ 𝑤 ∈ 𝐴 𝑤 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 )
32 29 31 bitr3i ⊢ ( ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 )
33 ordttop ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
34 12 33 syl ⊢ ( 𝜑 → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
35 34 adantr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top )
36 0opn ⊢ ( ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ∈ Top → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
37 35 36 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
39 eleq1 ⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = ∅ → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∅ ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
40 38 39 syl5ibrcom ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = ∅ → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
41 rabn0 ⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ ↔ ∃ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 )
42 breq1 ⊢ ( 𝑤 = 𝑦 → ( 𝑤 𝑅 𝑧 ↔ 𝑦 𝑅 𝑧 ) )
43 42 notbid ⊢ ( 𝑤 = 𝑦 → ( ¬ 𝑤 𝑅 𝑧 ↔ ¬ 𝑦 𝑅 𝑧 ) )
44 43 cbvrexvw ⊢ ( ∃ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 )
45 41 44 bitri ⊢ ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 )
46 2 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑅 ∈ TosetRel )
47 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → 𝐴 ⊆ 𝑋 )
48 47 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝑋 )
49 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → 𝑧 ∈ 𝑋 )
50 1 tsrlin ⊢ ( ( 𝑅 ∈ TosetRel ∧ 𝑦 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑦 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) )
51 46 48 49 50 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 𝑅 𝑧 ∨ 𝑧 𝑅 𝑦 ) )
52 51 ord ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 𝑅 𝑧 → 𝑧 𝑅 𝑦 ) )
53 an4 ⊢ ( ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) ) )
54 rabss ⊢ ( { 𝑧 ∈ 𝑋 ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) } ⊆ 𝐴 ↔ ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) )
55 4 54 sylib ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ∀ 𝑧 ∈ 𝑋 ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) )
56 55 r19.21bi ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) )
57 56 an32s ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) → 𝑧 ∈ 𝐴 ) )
58 57 impr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
59 53 58 sylan2b ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ 𝐴 )
60 brinxp ⊢ ( ( 𝑤 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑧 ↔ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
61 60 ancoms ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( 𝑤 𝑅 𝑧 ↔ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
62 61 notbid ⊢ ( ( 𝑧 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) → ( ¬ 𝑤 𝑅 𝑧 ↔ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 ) )
63 62 rabbidva ⊢ ( 𝑧 ∈ 𝐴 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } )
64 59 63 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } )
65 19 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) = 𝐴 )
66 65 rabeqdv ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } = { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } )
67 64 66 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } = { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } )
68 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V )
69 59 65 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → 𝑧 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) )
70 13 ordtopn1 ⊢ ( ( ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∈ V ∧ 𝑧 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
71 68 69 70 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ dom ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ∣ ¬ 𝑤 ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
72 67 71 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
73 72 anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 𝑅 𝑦 ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
74 73 expr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑧 𝑅 𝑦 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
75 52 74 syld ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
76 75 rexlimdva ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( ∃ 𝑦 ∈ 𝐴 ¬ 𝑦 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
77 45 76 biimtrid ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → ( { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
78 40 77 pm2.61dne ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑥 𝑅 𝑧 ) ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
79 78 rexlimdvaa ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝐴 𝑥 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
80 32 79 biimtrid ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( ¬ ∀ 𝑤 ∈ 𝐴 ¬ 𝑤 𝑅 𝑧 → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
81 28 80 pm2.61d ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → { 𝑤 ∈ 𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
82 10 81 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑋 ) → ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
83 82 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
84 2 dmexd ⊢ ( 𝜑 → dom 𝑅 ∈ V )
85 1 84 eqeltrid ⊢ ( 𝜑 → 𝑋 ∈ V )
86 rabexg ⊢ ( 𝑋 ∈ V → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V )
87 85 86 syl ⊢ ( 𝜑 → { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V )
88 87 ralrimivw ⊢ ( 𝜑 → ∀ 𝑧 ∈ 𝑋 { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V )
89 eqid ⊢ ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) = ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } )
90 ineq1 ⊢ ( 𝑣 = { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } → ( 𝑣 ∩ 𝐴 ) = ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) )
91 90 eleq1d ⊢ ( 𝑣 = { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } → ( ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
92 89 91 ralrnmptw ⊢ ( ∀ 𝑧 ∈ 𝑋 { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ V → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
93 88 92 syl ⊢ ( 𝜑 → ( ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ↔ ∀ 𝑧 ∈ 𝑋 ( { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
94 83 93 mpbird ⊢ ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝑋 ↦ { 𝑤 ∈ 𝑋 ∣ ¬ 𝑤 𝑅 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )