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 syl5bi ( ( ( 𝜑𝑧𝑋 ) ∧ ( 𝑥𝐴𝑥 𝑅 𝑧 ) ) → ( { 𝑤𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ≠ ∅ → { 𝑤𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
78 40 77 pm2.61dne ( ( ( 𝜑𝑧𝑋 ) ∧ ( 𝑥𝐴𝑥 𝑅 𝑧 ) ) → { 𝑤𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )
79 78 rexlimdvaa ( ( 𝜑𝑧𝑋 ) → ( ∃ 𝑥𝐴 𝑥 𝑅 𝑧 → { 𝑤𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( ordTop ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) ) )
80 32 79 syl5bi ( ( 𝜑𝑧𝑋 ) → ( ¬ ∀ 𝑤𝐴 ¬ 𝑤 𝑅 𝑧 → { 𝑤𝐴 ∣ ¬ 𝑤 𝑅 𝑧 } ∈ ( 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 ‘ ( 𝑅 ∩ ( 𝐴 × 𝐴 ) ) ) )