Metamath Proof Explorer

Theorem etaslts

Description: A restatement of noeta using set less-than. (Contributed by Scott Fenton, 10-Aug-2024)

Ref Expression
Assertion etaslts ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O

Proof

Step Hyp Ref Expression
1 sltsss1 ⊢ A ≪ s B → A ⊆ No
2 sltsex1 ⊢ A ≪ s B → A ∈ V
3 1 2 jca ⊢ A ≪ s B → A ⊆ No ∧ A ∈ V
4 sltsss2 ⊢ A ≪ s B → B ⊆ No
5 sltsex2 ⊢ A ≪ s B → B ∈ V
6 4 5 jca ⊢ A ≪ s B → B ⊆ No ∧ B ∈ V
7 sltssep ⊢ A ≪ s B → ∀ y ∈ A ∀ z ∈ B y < s z
8 3 6 7 3jca ⊢ A ≪ s B → A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ y ∈ A ∀ z ∈ B y < s z
9 8 3ad2ant1 ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ y ∈ A ∀ z ∈ B y < s z
10 3simpc ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → O ∈ On ∧ bday A ∪ B ⊆ O
11 noeta ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ y ∈ A ∀ z ∈ B y < s z ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O
12 9 10 11 syl2anc ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O
13 2 ad2antrr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ∈ V
14 vsnex ⊢ x ∈ V
15 13 14 jctir ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ∈ V ∧ x ∈ V
16 1 ad2antrr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ⊆ No
17 snssi ⊢ x ∈ No → x ⊆ No
18 17 ad2antrl ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → x ⊆ No
19 simprr1 ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∀ y ∈ A y < s x
20 vex ⊢ x ∈ V
21 breq2 ⊢ z = x → y < s z ↔ y < s x
22 20 21 ralsn ⊢ ∀ z ∈ x y < s z ↔ y < s x
23 22 ralbii ⊢ ∀ y ∈ A ∀ z ∈ x y < s z ↔ ∀ y ∈ A y < s x
24 19 23 sylibr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∀ y ∈ A ∀ z ∈ x y < s z
25 16 18 24 3jca ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
26 brslts ⊢ A ≪ s x ↔ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
27 15 25 26 sylanbrc ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ≪ s x
28 5 ad2antrr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → B ∈ V
29 28 14 jctil ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → x ∈ V ∧ B ∈ V
30 4 ad2antrr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → B ⊆ No
31 simprr2 ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∀ z ∈ B x < s z
32 breq1 ⊢ y = x → y < s z ↔ x < s z
33 32 ralbidv ⊢ y = x → ∀ z ∈ B y < s z ↔ ∀ z ∈ B x < s z
34 20 33 ralsn ⊢ ∀ y ∈ x ∀ z ∈ B y < s z ↔ ∀ z ∈ B x < s z
35 31 34 sylibr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∀ y ∈ x ∀ z ∈ B y < s z
36 18 30 35 3jca ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
37 brslts ⊢ x ≪ s B ↔ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
38 29 36 37 sylanbrc ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → x ≪ s B
39 simprr3 ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → bday ⁡ x ⊆ O
40 27 38 39 3jca ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No ∧ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O
41 40 expr ⊢ A ≪ s B ∧ O ∈ On ∧ x ∈ No → ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O
42 41 reximdva ⊢ A ≪ s B ∧ O ∈ On → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O
43 42 3adant3 ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ O → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O
44 12 43 mpd ⊢ A ≪ s B ∧ O ∈ On ∧ bday A ∪ B ⊆ O → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ O