Metamath Proof Explorer

Theorem prproropf1olem4

Description: Lemma 4 for prproropf1o . (Contributed by AV, 14-Mar-2023)

Ref Expression
Hypotheses prproropf1o.o ⊢ O = R ∩ V × V
prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
prproropf1o.f ⊢ F = p ∈ P ⟼ inf p V R sup p V R
Assertion prproropf1olem4 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → F ⁡ Z = F ⁡ W → Z = W

Proof

Step Hyp Ref Expression
1 prproropf1o.o ⊢ O = R ∩ V × V
2 prproropf1o.p ⊢ P = p ∈ 𝒫 V | p = 2
3 prproropf1o.f ⊢ F = p ∈ P ⟼ inf p V R sup p V R
4 infeq1 ⊢ p = Z → inf p V R = inf Z V R
5 supeq1 ⊢ p = Z → sup p V R = sup Z V R
6 4 5 opeq12d ⊢ p = Z → inf p V R sup p V R = inf Z V R sup Z V R
7 simp3 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → Z ∈ P
8 opex ⊢ inf Z V R sup Z V R ∈ V
9 8 a1i ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → inf Z V R sup Z V R ∈ V
10 3 6 7 9 fvmptd3 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → F ⁡ Z = inf Z V R sup Z V R
11 infeq1 ⊢ p = W → inf p V R = inf W V R
12 supeq1 ⊢ p = W → sup p V R = sup W V R
13 11 12 opeq12d ⊢ p = W → inf p V R sup p V R = inf W V R sup W V R
14 simp2 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → W ∈ P
15 opex ⊢ inf W V R sup W V R ∈ V
16 15 a1i ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → inf W V R sup W V R ∈ V
17 3 13 14 16 fvmptd3 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → F ⁡ W = inf W V R sup W V R
18 10 17 eqeq12d ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → F ⁡ Z = F ⁡ W ↔ inf Z V R sup Z V R = inf W V R sup W V R
19 2 prpair ⊢ Z ∈ P ↔ ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d
20 2 prpair ⊢ W ∈ P ↔ ∃ a ∈ V ∃ b ∈ V W = a b ∧ a ≠ b
21 id ⊢ R Or V → R Or V
22 21 infexd ⊢ R Or V → inf c d V R ∈ V
23 21 supexd ⊢ R Or V → sup c d V R ∈ V
24 22 23 jca ⊢ R Or V → inf c d V R ∈ V ∧ sup c d V R ∈ V
25 24 ad4antr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf c d V R ∈ V ∧ sup c d V R ∈ V
26 opthg ⊢ inf c d V R ∈ V ∧ sup c d V R ∈ V → inf c d V R sup c d V R = inf a b V R sup a b V R ↔ inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R
27 25 26 syl ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf c d V R sup c d V R = inf a b V R sup a b V R ↔ inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R
28 solin ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → a R b ∨ a = b ∨ b R a
29 infpr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = if a R b a b
30 29 3expb ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = if a R b a b
31 iftrue ⊢ a R b → if a R b a b = a
32 30 31 sylan9eqr ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = a
33 32 eqeq2d ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf c d V R = inf a b V R ↔ inf c d V R = a
34 suppr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = if b R a a b
35 34 3expb ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = if b R a a b
36 35 adantl ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = if b R a a b
37 sotric ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → a R b ↔ ¬ a = b ∨ b R a
38 ioran ⊢ ¬ a = b ∨ b R a ↔ ¬ a = b ∧ ¬ b R a
39 iffalse ⊢ ¬ b R a → if b R a a b = b
40 38 39 simplbiim ⊢ ¬ a = b ∨ b R a → if b R a a b = b
41 37 40 biimtrdi ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → a R b → if b R a a b = b
42 41 impcom ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → if b R a a b = b
43 36 42 eqtrd ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = b
44 43 eqeq2d ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → sup c d V R = sup a b V R ↔ sup c d V R = b
45 33 44 anbi12d ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R ↔ inf c d V R = a ∧ sup c d V R = b
46 45 adantr ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R ↔ inf c d V R = a ∧ sup c d V R = b
47 solin ⊢ R Or V ∧ c ∈ V ∧ d ∈ V → c R d ∨ c = d ∨ d R c
48 47 adantrr ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → c R d ∨ c = d ∨ d R c
49 simpl ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → R Or V
50 simprll ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → c ∈ V
51 simprlr ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → d ∈ V
52 infpr ⊢ R Or V ∧ c ∈ V ∧ d ∈ V → inf c d V R = if c R d c d
53 49 50 51 52 syl3anc ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = if c R d c d
54 iftrue ⊢ c R d → if c R d c d = c
55 53 54 sylan9eqr ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = c
56 55 eqeq1d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ↔ c = a
57 suppr ⊢ R Or V ∧ c ∈ V ∧ d ∈ V → sup c d V R = if d R c c d
58 49 50 51 57 syl3anc ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = if d R c c d
59 58 adantl ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = if d R c c d
60 sotric ⊢ R Or V ∧ c ∈ V ∧ d ∈ V → c R d ↔ ¬ c = d ∨ d R c
61 60 adantrr ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → c R d ↔ ¬ c = d ∨ d R c
62 ioran ⊢ ¬ c = d ∨ d R c ↔ ¬ c = d ∧ ¬ d R c
63 iffalse ⊢ ¬ d R c → if d R c c d = d
64 62 63 simplbiim ⊢ ¬ c = d ∨ d R c → if d R c c d = d
65 61 64 biimtrdi ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → c R d → if d R c c d = d
66 65 impcom ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → if d R c c d = d
67 59 66 eqtrd ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = d
68 67 eqeq1d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = b ↔ d = b
69 56 68 anbi12d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b ↔ c = a ∧ d = b
70 orc ⊢ c = a ∧ d = b → c = a ∧ d = b ∨ c = b ∧ d = a
71 69 70 biimtrdi ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
72 71 ex ⊢ c R d → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
73 eqneqall ⊢ c = d → c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
74 73 adantld ⊢ c = d → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
75 74 adantld ⊢ c = d → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
76 53 adantl ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = if c R d c d
77 76 eqeq1d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ↔ if c R d c d = a
78 iftrue ⊢ d R c → if d R c c d = c
79 58 78 sylan9eqr ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = c
80 79 eqeq1d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = b ↔ c = b
81 77 80 anbi12d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b ↔ if c R d c d = a ∧ c = b
82 simpl ⊢ c ∈ V ∧ d ∈ V ∧ c ≠ d → c ∈ V ∧ d ∈ V
83 82 ancomd ⊢ c ∈ V ∧ d ∈ V ∧ c ≠ d → d ∈ V ∧ c ∈ V
84 sotric ⊢ R Or V ∧ d ∈ V ∧ c ∈ V → d R c ↔ ¬ d = c ∨ c R d
85 83 84 sylan2 ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → d R c ↔ ¬ d = c ∨ c R d
86 ioran ⊢ ¬ d = c ∨ c R d ↔ ¬ d = c ∧ ¬ c R d
87 iffalse ⊢ ¬ c R d → if c R d c d = d
88 86 87 simplbiim ⊢ ¬ d = c ∨ c R d → if c R d c d = d
89 88 eqeq1d ⊢ ¬ d = c ∨ c R d → if c R d c d = a ↔ d = a
90 85 89 biimtrdi ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → d R c → if c R d c d = a ↔ d = a
91 90 impcom ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → if c R d c d = a ↔ d = a
92 91 anbi1d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → if c R d c d = a ∧ c = b ↔ d = a ∧ c = b
93 olc ⊢ c = b ∧ d = a → c = a ∧ d = b ∨ c = b ∧ d = a
94 93 ancoms ⊢ d = a ∧ c = b → c = a ∧ d = b ∨ c = b ∧ d = a
95 92 94 biimtrdi ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → if c R d c d = a ∧ c = b → c = a ∧ d = b ∨ c = b ∧ d = a
96 81 95 sylbid ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
97 96 ex ⊢ d R c → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
98 72 75 97 3jaoi ⊢ c R d ∨ c = d ∨ d R c → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
99 48 98 mpcom ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
100 99 ex ⊢ R Or V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
101 100 ad2antrl ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
102 101 imp ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = a ∧ sup c d V R = b → c = a ∧ d = b ∨ c = b ∧ d = a
103 46 102 sylbid ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
104 103 ex ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
105 104 a1d ⊢ a R b ∧ R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
106 105 ex ⊢ a R b → R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
107 eqneqall ⊢ a = b → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
108 107 a1d ⊢ a = b → R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
109 30 adantl ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = if a R b a b
110 sotric ⊢ R Or V ∧ b ∈ V ∧ a ∈ V → b R a ↔ ¬ b = a ∨ a R b
111 110 ancom2s ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → b R a ↔ ¬ b = a ∨ a R b
112 ioran ⊢ ¬ b = a ∨ a R b ↔ ¬ b = a ∧ ¬ a R b
113 iffalse ⊢ ¬ a R b → if a R b a b = b
114 112 113 simplbiim ⊢ ¬ b = a ∨ a R b → if a R b a b = b
115 111 114 biimtrdi ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → b R a → if a R b a b = b
116 115 impcom ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → if a R b a b = b
117 109 116 eqtrd ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf a b V R = b
118 117 eqeq2d ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf c d V R = inf a b V R ↔ inf c d V R = b
119 iftrue ⊢ b R a → if b R a a b = a
120 35 119 sylan9eqr ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → sup a b V R = a
121 120 eqeq2d ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → sup c d V R = sup a b V R ↔ sup c d V R = a
122 118 121 anbi12d ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R ↔ inf c d V R = b ∧ sup c d V R = a
123 122 adantr ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R ↔ inf c d V R = b ∧ sup c d V R = a
124 55 eqeq1d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ↔ c = b
125 67 eqeq1d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = a ↔ d = a
126 124 125 anbi12d ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a ↔ c = b ∧ d = a
127 126 93 biimtrdi ⊢ c R d ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
128 127 ex ⊢ c R d → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
129 eqneqall ⊢ c = d → c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
130 129 adantld ⊢ c = d → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
131 130 adantld ⊢ c = d → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
132 85 88 biimtrdi ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → d R c → if c R d c d = d
133 132 impcom ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → if c R d c d = d
134 76 133 eqtrd ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = d
135 134 eqeq1d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ↔ d = b
136 79 eqeq1d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → sup c d V R = a ↔ c = a
137 135 136 anbi12d ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a ↔ d = b ∧ c = a
138 70 ancoms ⊢ d = b ∧ c = a → c = a ∧ d = b ∨ c = b ∧ d = a
139 137 138 biimtrdi ⊢ d R c ∧ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
140 139 ex ⊢ d R c → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
141 128 131 140 3jaoi ⊢ c R d ∨ c = d ∨ d R c → R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
142 48 141 mpcom ⊢ R Or V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
143 142 ex ⊢ R Or V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
144 143 ad2antrl ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
145 144 imp ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = b ∧ sup c d V R = a → c = a ∧ d = b ∨ c = b ∧ d = a
146 123 145 sylbid ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V ∧ c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
147 146 ex ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
148 147 a1d ⊢ b R a ∧ R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
149 148 ex ⊢ b R a → R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
150 106 108 149 3jaoi ⊢ a R b ∨ a = b ∨ b R a → R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
151 28 150 mpcom ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
152 151 adantld ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → W = a b ∧ a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
153 152 imp ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b → c ∈ V ∧ d ∈ V ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
154 153 expdimp ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
155 154 adantld ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → Z = c d ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
156 155 imp ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c = a ∧ d = b ∨ c = b ∧ d = a
157 vex ⊢ c ∈ V
158 vex ⊢ d ∈ V
159 vex ⊢ a ∈ V
160 vex ⊢ b ∈ V
161 157 158 159 160 preq12b ⊢ c d = a b ↔ c = a ∧ d = b ∨ c = b ∧ d = a
162 156 161 imbitrrdi ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf c d V R = inf a b V R ∧ sup c d V R = sup a b V R → c d = a b
163 27 162 sylbid ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
164 infeq1 ⊢ Z = c d → inf Z V R = inf c d V R
165 supeq1 ⊢ Z = c d → sup Z V R = sup c d V R
166 164 165 opeq12d ⊢ Z = c d → inf Z V R sup Z V R = inf c d V R sup c d V R
167 infeq1 ⊢ W = a b → inf W V R = inf a b V R
168 supeq1 ⊢ W = a b → sup W V R = sup a b V R
169 167 168 opeq12d ⊢ W = a b → inf W V R sup W V R = inf a b V R sup a b V R
170 166 169 eqeqan12rd ⊢ W = a b ∧ Z = c d → inf Z V R sup Z V R = inf W V R sup W V R ↔ inf c d V R sup c d V R = inf a b V R sup a b V R
171 eqeq12 ⊢ Z = c d ∧ W = a b → Z = W ↔ c d = a b
172 171 ancoms ⊢ W = a b ∧ Z = c d → Z = W ↔ c d = a b
173 170 172 imbi12d ⊢ W = a b ∧ Z = c d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
174 173 ex ⊢ W = a b → Z = c d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
175 174 ad2antrl ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b → Z = c d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
176 175 adantr ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → Z = c d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
177 176 com12 ⊢ Z = c d → R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
178 177 adantr ⊢ Z = c d ∧ c ≠ d → R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
179 178 impcom ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W ↔ inf c d V R sup c d V R = inf a b V R sup a b V R → c d = a b
180 163 179 mpbird ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V ∧ Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
181 180 ex ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b ∧ c ∈ V ∧ d ∈ V → Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
182 181 rexlimdvva ⊢ R Or V ∧ a ∈ V ∧ b ∈ V ∧ W = a b ∧ a ≠ b → ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
183 182 ex ⊢ R Or V ∧ a ∈ V ∧ b ∈ V → W = a b ∧ a ≠ b → ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
184 183 rexlimdvva ⊢ R Or V → ∃ a ∈ V ∃ b ∈ V W = a b ∧ a ≠ b → ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
185 184 com13 ⊢ ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d → ∃ a ∈ V ∃ b ∈ V W = a b ∧ a ≠ b → R Or V → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
186 20 185 biimtrid ⊢ ∃ c ∈ V ∃ d ∈ V Z = c d ∧ c ≠ d → W ∈ P → R Or V → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
187 19 186 sylbi ⊢ Z ∈ P → W ∈ P → R Or V → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
188 187 3imp31 ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → inf Z V R sup Z V R = inf W V R sup W V R → Z = W
189 18 188 sylbid ⊢ R Or V ∧ W ∈ P ∧ Z ∈ P → F ⁡ Z = F ⁡ W → Z = W