MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  slerec Structured version   Visualization version   GIF version

Theorem slerec 27666
Description: A comparison law for surreals considered as cuts of sets of surreals. Definition from [Conway] p. 4. Theorem 4 of [Alling] p. 186. Theorem 2.5 of [Gonshor] p. 9. (Contributed by Scott Fenton, 11-Dec-2021.)
Assertion
Ref Expression
slerec (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷))) → (𝑋 â‰Īs 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s 𝑌)))
Distinct variable groups:   ðī,𝑎,𝑑   ðĩ,𝑎,𝑑   ðķ,𝑎,𝑑   𝐷,𝑎,𝑑   𝑋,𝑎,𝑑   𝑌,𝑎,𝑑

Proof of Theorem slerec
Dummy variables 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 scutcl 27649 . . . . . . . 8 (ðī <<s ðĩ → (ðī |s ðĩ) ∈ No )
21ad3antrrr 727 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → (ðī |s ðĩ) ∈ No )
3 scutcl 27649 . . . . . . . 8 (ðķ <<s 𝐷 → (ðķ |s 𝐷) ∈ No )
43ad3antlr 728 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → (ðķ |s 𝐷) ∈ No )
5 ssltss2 27636 . . . . . . . . 9 (ðķ <<s 𝐷 → 𝐷 ⊆ No )
65ad2antlr 724 . . . . . . . 8 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → 𝐷 ⊆ No )
76sselda 3982 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → 𝑑 ∈ No )
8 simplr 766 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷))
9 scutcut 27648 . . . . . . . . . . . 12 (ðķ <<s 𝐷 → ((ðķ |s 𝐷) ∈ No ∧ ðķ <<s {(ðķ |s 𝐷)} ∧ {(ðķ |s 𝐷)} <<s 𝐷))
109simp3d 1143 . . . . . . . . . . 11 (ðķ <<s 𝐷 → {(ðķ |s 𝐷)} <<s 𝐷)
1110ad2antlr 724 . . . . . . . . . 10 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → {(ðķ |s 𝐷)} <<s 𝐷)
12 ssltsep 27637 . . . . . . . . . 10 ({(ðķ |s 𝐷)} <<s 𝐷 → ∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑)
1311, 12syl 17 . . . . . . . . 9 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑)
14 ovex 7445 . . . . . . . . . 10 (ðķ |s 𝐷) ∈ V
15 breq1 5151 . . . . . . . . . . 11 (𝑎 = (ðķ |s 𝐷) → (𝑎 <s 𝑑 ↔ (ðķ |s 𝐷) <s 𝑑))
1615ralbidv 3176 . . . . . . . . . 10 (𝑎 = (ðķ |s 𝐷) → (∀𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀𝑑 ∈ 𝐷 (ðķ |s 𝐷) <s 𝑑))
1714, 16ralsn 4685 . . . . . . . . 9 (∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀𝑑 ∈ 𝐷 (ðķ |s 𝐷) <s 𝑑)
1813, 17sylib 217 . . . . . . . 8 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ∀𝑑 ∈ 𝐷 (ðķ |s 𝐷) <s 𝑑)
1918r19.21bi 3247 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → (ðķ |s 𝐷) <s 𝑑)
202, 4, 7, 8, 19slelttrd 27608 . . . . . 6 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑑 ∈ 𝐷) → (ðī |s ðĩ) <s 𝑑)
2120ralrimiva 3145 . . . . 5 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑)
22 ssltss1 27635 . . . . . . . . . 10 (ðī <<s ðĩ → ðī ⊆ No )
2322adantr 480 . . . . . . . . 9 ((ðī <<s ðĩ ∧ ðķ <<s 𝐷) → ðī ⊆ No )
2423adantr 480 . . . . . . . 8 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ðī ⊆ No )
2524sselda 3982 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → 𝑎 ∈ No )
261ad3antrrr 727 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → (ðī |s ðĩ) ∈ No )
273ad3antlr 728 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → (ðķ |s 𝐷) ∈ No )
28 scutcut 27648 . . . . . . . . . . . . 13 (ðī <<s ðĩ → ((ðī |s ðĩ) ∈ No ∧ ðī <<s {(ðī |s ðĩ)} ∧ {(ðī |s ðĩ)} <<s ðĩ))
2928simp2d 1142 . . . . . . . . . . . 12 (ðī <<s ðĩ → ðī <<s {(ðī |s ðĩ)})
3029adantr 480 . . . . . . . . . . 11 ((ðī <<s ðĩ ∧ ðķ <<s 𝐷) → ðī <<s {(ðī |s ðĩ)})
3130adantr 480 . . . . . . . . . 10 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ðī <<s {(ðī |s ðĩ)})
32 ssltsep 27637 . . . . . . . . . 10 (ðī <<s {(ðī |s ðĩ)} → ∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðī |s ðĩ)}𝑎 <s 𝑑)
3331, 32syl 17 . . . . . . . . 9 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðī |s ðĩ)}𝑎 <s 𝑑)
3433r19.21bi 3247 . . . . . . . 8 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → ∀𝑑 ∈ {(ðī |s ðĩ)}𝑎 <s 𝑑)
35 ovex 7445 . . . . . . . . 9 (ðī |s ðĩ) ∈ V
36 breq2 5152 . . . . . . . . 9 (𝑑 = (ðī |s ðĩ) → (𝑎 <s 𝑑 ↔ 𝑎 <s (ðī |s ðĩ)))
3735, 36ralsn 4685 . . . . . . . 8 (∀𝑑 ∈ {(ðī |s ðĩ)}𝑎 <s 𝑑 ↔ 𝑎 <s (ðī |s ðĩ))
3834, 37sylib 217 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → 𝑎 <s (ðī |s ðĩ))
39 simplr 766 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷))
4025, 26, 27, 38, 39sltletrd 27607 . . . . . 6 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) ∧ 𝑎 ∈ ðī) → 𝑎 <s (ðķ |s 𝐷))
4140ralrimiva 3145 . . . . 5 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))
4221, 41jca 511 . . . 4 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)) → (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷)))
43 bdayelon 27623 . . . . . . 7 ( bday ‘(ðī |s ðĩ)) ∈ On
4443onordi 6475 . . . . . 6 Ord ( bday ‘(ðī |s ðĩ))
45 ordn2lp 6384 . . . . . 6 (Ord ( bday ‘(ðī |s ðĩ)) → ÂŽ (( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)) ∧ ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ))))
4644, 45ax-mp 5 . . . . 5 ÂŽ (( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)) ∧ ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ)))
473ad2antlr 724 . . . . . . 7 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → (ðķ |s 𝐷) ∈ No )
481adantr 480 . . . . . . . 8 ((ðī <<s ðĩ ∧ ðķ <<s 𝐷) → (ðī |s ðĩ) ∈ No )
4948adantr 480 . . . . . . 7 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → (ðī |s ðĩ) ∈ No )
50 sltnle 27600 . . . . . . 7 (((ðķ |s 𝐷) ∈ No ∧ (ðī |s ðĩ) ∈ No ) → ((ðķ |s 𝐷) <s (ðī |s ðĩ) ↔ ÂŽ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)))
5147, 49, 50syl2anc 583 . . . . . 6 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → ((ðķ |s 𝐷) <s (ðī |s ðĩ) ↔ ÂŽ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)))
523ad3antlr 728 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðķ |s 𝐷) ∈ No )
53 ssltex1 27633 . . . . . . . . . . . 12 (ðī <<s ðĩ → ðī ∈ V)
5453ad3antrrr 727 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðī ∈ V)
55 snex 5431 . . . . . . . . . . 11 {(ðķ |s 𝐷)} ∈ V
5654, 55jctir 520 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðī ∈ V ∧ {(ðķ |s 𝐷)} ∈ V))
5722ad3antrrr 727 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðī ⊆ No )
5852snssd 4812 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → {(ðķ |s 𝐷)} ⊆ No )
59 simplrr 775 . . . . . . . . . . . 12 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))
60 breq2 5152 . . . . . . . . . . . . . 14 (𝑑 = (ðķ |s 𝐷) → (𝑎 <s 𝑑 ↔ 𝑎 <s (ðķ |s 𝐷)))
6114, 60ralsn 4685 . . . . . . . . . . . . 13 (∀𝑑 ∈ {(ðķ |s 𝐷)}𝑎 <s 𝑑 ↔ 𝑎 <s (ðķ |s 𝐷))
6261ralbii 3092 . . . . . . . . . . . 12 (∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑎 <s 𝑑 ↔ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))
6359, 62sylibr 233 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑎 <s 𝑑)
6457, 58, 633jca 1127 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðī ⊆ No ∧ {(ðķ |s 𝐷)} ⊆ No ∧ ∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑎 <s 𝑑))
65 brsslt 27632 . . . . . . . . . 10 (ðī <<s {(ðķ |s 𝐷)} ↔ ((ðī ∈ V ∧ {(ðķ |s 𝐷)} ∈ V) ∧ (ðī ⊆ No ∧ {(ðķ |s 𝐷)} ⊆ No ∧ ∀𝑎 ∈ ðī ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑎 <s 𝑑)))
6656, 64, 65sylanbrc 582 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðī <<s {(ðķ |s 𝐷)})
67 ssltex2 27634 . . . . . . . . . . . 12 (ðī <<s ðĩ → ðĩ ∈ V)
6867ad3antrrr 727 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðĩ ∈ V)
6968, 55jctil 519 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ({(ðķ |s 𝐷)} ∈ V ∧ ðĩ ∈ V))
70 ssltss2 27636 . . . . . . . . . . . 12 (ðī <<s ðĩ → ðĩ ⊆ No )
7170ad3antrrr 727 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðĩ ⊆ No )
7252adantr 480 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → (ðķ |s 𝐷) ∈ No )
7348ad3antrrr 727 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → (ðī |s ðĩ) ∈ No )
7471sselda 3982 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → 𝑏 ∈ No )
75 simplr 766 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → (ðķ |s 𝐷) <s (ðī |s ðĩ))
7628simp3d 1143 . . . . . . . . . . . . . . . . . 18 (ðī <<s ðĩ → {(ðī |s ðĩ)} <<s ðĩ)
7776ad3antrrr 727 . . . . . . . . . . . . . . . . 17 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → {(ðī |s ðĩ)} <<s ðĩ)
78 ssltsep 27637 . . . . . . . . . . . . . . . . 17 ({(ðī |s ðĩ)} <<s ðĩ → ∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏)
7977, 78syl 17 . . . . . . . . . . . . . . . 16 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏)
80 breq1 5151 . . . . . . . . . . . . . . . . . 18 (𝑎 = (ðī |s ðĩ) → (𝑎 <s 𝑏 ↔ (ðī |s ðĩ) <s 𝑏))
8180ralbidv 3176 . . . . . . . . . . . . . . . . 17 (𝑎 = (ðī |s ðĩ) → (∀𝑏 ∈ ðĩ 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ ðĩ (ðī |s ðĩ) <s 𝑏))
8235, 81ralsn 4685 . . . . . . . . . . . . . . . 16 (∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ ðĩ (ðī |s ðĩ) <s 𝑏)
8379, 82sylib 217 . . . . . . . . . . . . . . 15 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑏 ∈ ðĩ (ðī |s ðĩ) <s 𝑏)
8483r19.21bi 3247 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → (ðī |s ðĩ) <s 𝑏)
8572, 73, 74, 75, 84slttrd 27606 . . . . . . . . . . . . 13 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑏 ∈ ðĩ) → (ðķ |s 𝐷) <s 𝑏)
8685ralrimiva 3145 . . . . . . . . . . . 12 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑏 ∈ ðĩ (ðķ |s 𝐷) <s 𝑏)
87 breq1 5151 . . . . . . . . . . . . . 14 (𝑎 = (ðķ |s 𝐷) → (𝑎 <s 𝑏 ↔ (ðķ |s 𝐷) <s 𝑏))
8887ralbidv 3176 . . . . . . . . . . . . 13 (𝑎 = (ðķ |s 𝐷) → (∀𝑏 ∈ ðĩ 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ ðĩ (ðķ |s 𝐷) <s 𝑏))
8914, 88ralsn 4685 . . . . . . . . . . . 12 (∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏 ↔ ∀𝑏 ∈ ðĩ (ðķ |s 𝐷) <s 𝑏)
9086, 89sylibr 233 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏)
9158, 71, 903jca 1127 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ({(ðķ |s 𝐷)} ⊆ No ∧ ðĩ ⊆ No ∧ ∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏))
92 brsslt 27632 . . . . . . . . . 10 ({(ðķ |s 𝐷)} <<s ðĩ ↔ (({(ðķ |s 𝐷)} ∈ V ∧ ðĩ ∈ V) ∧ ({(ðķ |s 𝐷)} ⊆ No ∧ ðĩ ⊆ No ∧ ∀𝑎 ∈ {(ðķ |s 𝐷)}∀𝑏 ∈ ðĩ 𝑎 <s 𝑏)))
9369, 91, 92sylanbrc 582 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → {(ðķ |s 𝐷)} <<s ðĩ)
94 sltirr 27593 . . . . . . . . . . . . . 14 ((ðī |s ðĩ) ∈ No → ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ))
9549, 94syl 17 . . . . . . . . . . . . 13 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ))
96 breq1 5151 . . . . . . . . . . . . . 14 ((ðī |s ðĩ) = (ðķ |s 𝐷) → ((ðī |s ðĩ) <s (ðī |s ðĩ) ↔ (ðķ |s 𝐷) <s (ðī |s ðĩ)))
9796notbid 318 . . . . . . . . . . . . 13 ((ðī |s ðĩ) = (ðķ |s 𝐷) → (ÂŽ (ðī |s ðĩ) <s (ðī |s ðĩ) ↔ ÂŽ (ðķ |s 𝐷) <s (ðī |s ðĩ)))
9895, 97syl5ibcom 244 . . . . . . . . . . . 12 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → ((ðī |s ðĩ) = (ðķ |s 𝐷) → ÂŽ (ðķ |s 𝐷) <s (ðī |s ðĩ)))
9998necon2ad 2954 . . . . . . . . . . 11 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → ((ðķ |s 𝐷) <s (ðī |s ðĩ) → (ðī |s ðĩ) ≠ (ðķ |s 𝐷)))
10099imp 406 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðī |s ðĩ) ≠ (ðķ |s 𝐷))
101100necomd 2995 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðķ |s 𝐷) ≠ (ðī |s ðĩ))
102 scutbdaylt 27665 . . . . . . . . 9 (((ðķ |s 𝐷) ∈ No ∧ (ðī <<s {(ðķ |s 𝐷)} ∧ {(ðķ |s 𝐷)} <<s ðĩ) ∧ (ðķ |s 𝐷) ≠ (ðī |s ðĩ)) → ( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)))
10352, 66, 93, 101, 102syl121anc 1374 . . . . . . . 8 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)))
1041ad3antrrr 727 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðī |s ðĩ) ∈ No )
105 ssltex1 27633 . . . . . . . . . . . 12 (ðķ <<s 𝐷 → ðķ ∈ V)
106105ad3antlr 728 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðķ ∈ V)
107 snex 5431 . . . . . . . . . . 11 {(ðī |s ðĩ)} ∈ V
108106, 107jctir 520 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðķ ∈ V ∧ {(ðī |s ðĩ)} ∈ V))
109 ssltss1 27635 . . . . . . . . . . . 12 (ðķ <<s 𝐷 → ðķ ⊆ No )
110109ad3antlr 728 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðķ ⊆ No )
111104snssd 4812 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → {(ðī |s ðĩ)} ⊆ No )
112110sselda 3982 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → 𝑐 ∈ No )
11352adantr 480 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → (ðķ |s 𝐷) ∈ No )
11448ad3antrrr 727 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → (ðī |s ðĩ) ∈ No )
1159simp2d 1142 . . . . . . . . . . . . . . . . . 18 (ðķ <<s 𝐷 → ðķ <<s {(ðķ |s 𝐷)})
116115ad3antlr 728 . . . . . . . . . . . . . . . . 17 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðķ <<s {(ðķ |s 𝐷)})
117 ssltsep 27637 . . . . . . . . . . . . . . . . 17 (ðķ <<s {(ðķ |s 𝐷)} → ∀𝑐 ∈ ðķ ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑐 <s 𝑑)
118116, 117syl 17 . . . . . . . . . . . . . . . 16 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑐 ∈ ðķ ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑐 <s 𝑑)
119118r19.21bi 3247 . . . . . . . . . . . . . . 15 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → ∀𝑑 ∈ {(ðķ |s 𝐷)}𝑐 <s 𝑑)
120 breq2 5152 . . . . . . . . . . . . . . . 16 (𝑑 = (ðķ |s 𝐷) → (𝑐 <s 𝑑 ↔ 𝑐 <s (ðķ |s 𝐷)))
12114, 120ralsn 4685 . . . . . . . . . . . . . . 15 (∀𝑑 ∈ {(ðķ |s 𝐷)}𝑐 <s 𝑑 ↔ 𝑐 <s (ðķ |s 𝐷))
122119, 121sylib 217 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → 𝑐 <s (ðķ |s 𝐷))
123 simplr 766 . . . . . . . . . . . . . 14 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → (ðķ |s 𝐷) <s (ðī |s ðĩ))
124112, 113, 114, 122, 123slttrd 27606 . . . . . . . . . . . . 13 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → 𝑐 <s (ðī |s ðĩ))
125 breq2 5152 . . . . . . . . . . . . . 14 (𝑎 = (ðī |s ðĩ) → (𝑐 <s 𝑎 ↔ 𝑐 <s (ðī |s ðĩ)))
12635, 125ralsn 4685 . . . . . . . . . . . . 13 (∀𝑎 ∈ {(ðī |s ðĩ)}𝑐 <s 𝑎 ↔ 𝑐 <s (ðī |s ðĩ))
127124, 126sylibr 233 . . . . . . . . . . . 12 (((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) ∧ 𝑐 ∈ ðķ) → ∀𝑎 ∈ {(ðī |s ðĩ)}𝑐 <s 𝑎)
128127ralrimiva 3145 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑐 ∈ ðķ ∀𝑎 ∈ {(ðī |s ðĩ)}𝑐 <s 𝑎)
129110, 111, 1283jca 1127 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (ðķ ⊆ No ∧ {(ðī |s ðĩ)} ⊆ No ∧ ∀𝑐 ∈ ðķ ∀𝑎 ∈ {(ðī |s ðĩ)}𝑐 <s 𝑎))
130 brsslt 27632 . . . . . . . . . 10 (ðķ <<s {(ðī |s ðĩ)} ↔ ((ðķ ∈ V ∧ {(ðī |s ðĩ)} ∈ V) ∧ (ðķ ⊆ No ∧ {(ðī |s ðĩ)} ⊆ No ∧ ∀𝑐 ∈ ðķ ∀𝑎 ∈ {(ðī |s ðĩ)}𝑐 <s 𝑎)))
131108, 129, 130sylanbrc 582 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ðķ <<s {(ðī |s ðĩ)})
132 ssltex2 27634 . . . . . . . . . . . 12 (ðķ <<s 𝐷 → 𝐷 ∈ V)
133132ad3antlr 728 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → 𝐷 ∈ V)
134133, 107jctil 519 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ({(ðī |s ðĩ)} ∈ V ∧ 𝐷 ∈ V))
1355ad3antlr 728 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → 𝐷 ⊆ No )
136 simplrl 774 . . . . . . . . . . . 12 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑)
137 breq1 5151 . . . . . . . . . . . . . 14 (𝑎 = (ðī |s ðĩ) → (𝑎 <s 𝑑 ↔ (ðī |s ðĩ) <s 𝑑))
138137ralbidv 3176 . . . . . . . . . . . . 13 (𝑎 = (ðī |s ðĩ) → (∀𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑))
13935, 138ralsn 4685 . . . . . . . . . . . 12 (∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑 ↔ ∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑)
140136, 139sylibr 233 . . . . . . . . . . 11 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑)
141111, 135, 1403jca 1127 . . . . . . . . . 10 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ({(ðī |s ðĩ)} ⊆ No ∧ 𝐷 ⊆ No ∧ ∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑))
142 brsslt 27632 . . . . . . . . . 10 ({(ðī |s ðĩ)} <<s 𝐷 ↔ (({(ðī |s ðĩ)} ∈ V ∧ 𝐷 ∈ V) ∧ ({(ðī |s ðĩ)} ⊆ No ∧ 𝐷 ⊆ No ∧ ∀𝑎 ∈ {(ðī |s ðĩ)}∀𝑑 ∈ 𝐷 𝑎 <s 𝑑)))
143134, 141, 142sylanbrc 582 . . . . . . . . 9 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → {(ðī |s ðĩ)} <<s 𝐷)
144 scutbdaylt 27665 . . . . . . . . 9 (((ðī |s ðĩ) ∈ No ∧ (ðķ <<s {(ðī |s ðĩ)} ∧ {(ðī |s ðĩ)} <<s 𝐷) ∧ (ðī |s ðĩ) ≠ (ðķ |s 𝐷)) → ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ)))
145104, 131, 143, 100, 144syl121anc 1374 . . . . . . . 8 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ)))
146103, 145jca 511 . . . . . . 7 ((((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) ∧ (ðķ |s 𝐷) <s (ðī |s ðĩ)) → (( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)) ∧ ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ))))
147146ex 412 . . . . . 6 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → ((ðķ |s 𝐷) <s (ðī |s ðĩ) → (( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)) ∧ ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ)))))
14851, 147sylbird 260 . . . . 5 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → (ÂŽ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷) → (( bday ‘(ðī |s ðĩ)) ∈ ( bday ‘(ðķ |s 𝐷)) ∧ ( bday ‘(ðķ |s 𝐷)) ∈ ( bday ‘(ðī |s ðĩ)))))
14946, 148mt3i 149 . . . 4 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))) → (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷))
15042, 149impbida 798 . . 3 ((ðī <<s ðĩ ∧ ðķ <<s 𝐷) → ((ðī |s ðĩ) â‰Īs (ðķ |s 𝐷) ↔ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))))
151 breq12 5153 . . . 4 ((𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷)) → (𝑋 â‰Īs 𝑌 ↔ (ðī |s ðĩ) â‰Īs (ðķ |s 𝐷)))
152 breq1 5151 . . . . . 6 (𝑋 = (ðī |s ðĩ) → (𝑋 <s 𝑑 ↔ (ðī |s ðĩ) <s 𝑑))
153152ralbidv 3176 . . . . 5 (𝑋 = (ðī |s ðĩ) → (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ↔ ∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑))
154 breq2 5152 . . . . . 6 (𝑌 = (ðķ |s 𝐷) → (𝑎 <s 𝑌 ↔ 𝑎 <s (ðķ |s 𝐷)))
155154ralbidv 3176 . . . . 5 (𝑌 = (ðķ |s 𝐷) → (∀𝑎 ∈ ðī 𝑎 <s 𝑌 ↔ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷)))
156153, 155bi2anan9 636 . . . 4 ((𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷)) → ((∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s 𝑌) ↔ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷))))
157151, 156bibi12d 345 . . 3 ((𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷)) → ((𝑋 â‰Īs 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s 𝑌)) ↔ ((ðī |s ðĩ) â‰Īs (ðķ |s 𝐷) ↔ (∀𝑑 ∈ 𝐷 (ðī |s ðĩ) <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s (ðķ |s 𝐷)))))
158150, 157imbitrrid 245 . 2 ((𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷)) → ((ðī <<s ðĩ ∧ ðķ <<s 𝐷) → (𝑋 â‰Īs 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s 𝑌))))
159158impcom 407 1 (((ðī <<s ðĩ ∧ ðķ <<s 𝐷) ∧ (𝑋 = (ðī |s ðĩ) ∧ 𝑌 = (ðķ |s 𝐷))) → (𝑋 â‰Īs 𝑌 ↔ (∀𝑑 ∈ 𝐷 𝑋 <s 𝑑 ∧ ∀𝑎 ∈ ðī 𝑎 <s 𝑌)))
Colors of variables: wff setvar class
Syntax hints:  ÂŽ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1086   = wceq 1540   ∈ wcel 2105   ≠ wne 2939  âˆ€wral 3060  Vcvv 3473   ⊆ wss 3948  {csn 4628   class class class wbr 5148  Ord word 6363  â€˜cfv 6543  (class class class)co 7412   No csur 27487   <s cslt 27488   bday cbday 27489   â‰Īs csle 27591   <<s csslt 27627   |s cscut 27629
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3375  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-pss 3967  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-tp 4633  df-op 4635  df-uni 4909  df-int 4951  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5574  df-eprel 5580  df-po 5588  df-so 5589  df-fr 5631  df-we 5633  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ord 6367  df-on 6368  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7368  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1o 8472  df-2o 8473  df-no 27490  df-slt 27491  df-bday 27492  df-sle 27592  df-sslt 27628  df-scut 27630
This theorem is referenced by:  sltrec  27667
  Copyright terms: Public domain W3C validator