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