Metamath Proof Explorer

Theorem ordtrest2NEWlem

Description: Lemma for ordtrest2NEW . (Contributed by Mario Carneiro, 9-Sep-2015) (Revised by Thierry Arnoux, 11-Sep-2018)

Ref Expression
Hypotheses ordtNEW.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
ordtNEW.l ⊢ ≤ = ( ( le ‘ 𝐾 ) ∩ ( 𝐵 × 𝐵 ) )
ordtrest2NEW.2 ⊢ ( 𝜑 → 𝐾 ∈ Toset )
ordtrest2NEW.3 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
ordtrest2NEW.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → { 𝑧 ∈ 𝐵 ∣ ( 𝑥 ≤ 𝑧 ∧ 𝑧 ≤ 𝑦 ) } ⊆ 𝐴 )
Assertion ordtrest2NEWlem ( 𝜑 → ∀ 𝑣 ∈ ran ( 𝑧 ∈ 𝐵 ↦ { 𝑤 ∈ 𝐵 ∣ ¬ 𝑤 ≤ 𝑧 } ) ( 𝑣 ∩ 𝐴 ) ∈ ( ordTop ‘ ( ≤ ∩ ( 𝐴 × 𝐴 ) ) ) )

Proof

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