Metamath Proof Explorer

Theorem etasslt

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

Ref Expression
Assertion etasslt ⊢ A ≪ s B → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B

Proof

Step Hyp Ref Expression
1 ssltss1 ⊢ A ≪ s B → A ⊆ No
2 ssltex1 ⊢ A ≪ s B → A ∈ V
3 ssltss2 ⊢ A ≪ s B → B ⊆ No
4 ssltex2 ⊢ A ≪ s B → B ∈ V
5 ssltsep ⊢ A ≪ s B → ∀ y ∈ A ∀ z ∈ B y < s z
6 noeta ⊢ A ⊆ No ∧ A ∈ V ∧ B ⊆ No ∧ B ∈ V ∧ ∀ y ∈ A ∀ z ∈ B y < s z → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B
7 1 2 3 4 5 6 syl221anc ⊢ A ≪ s B → ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B
8 brsslt ⊢ A ≪ s x ↔ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
9 df-3an ⊢ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z ↔ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
10 9 bianass ⊢ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z ↔ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
11 8 10 bitri ⊢ A ≪ s x ↔ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
12 2 adantr ⊢ A ≪ s B ∧ x ∈ No → A ∈ V
13 snex ⊢ x ∈ V
14 12 13 jctir ⊢ A ≪ s B ∧ x ∈ No → A ∈ V ∧ x ∈ V
15 1 adantr ⊢ A ≪ s B ∧ x ∈ No → A ⊆ No
16 snssi ⊢ x ∈ No → x ⊆ No
17 16 adantl ⊢ A ≪ s B ∧ x ∈ No → x ⊆ No
18 14 15 17 jca32 ⊢ A ≪ s B ∧ x ∈ No → A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No
19 18 biantrurd ⊢ A ≪ s B ∧ x ∈ No → ∀ y ∈ A ∀ z ∈ x y < s z ↔ A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z
20 19 bicomd ⊢ A ≪ s B ∧ x ∈ No → A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z ↔ ∀ y ∈ A ∀ z ∈ x y < s z
21 vex ⊢ x ∈ V
22 breq2 ⊢ z = x → y < s z ↔ y < s x
23 21 22 ralsn ⊢ ∀ z ∈ x y < s z ↔ y < s x
24 23 ralbii ⊢ ∀ y ∈ A ∀ z ∈ x y < s z ↔ ∀ y ∈ A y < s x
25 20 24 syl6bb ⊢ A ≪ s B ∧ x ∈ No → A ∈ V ∧ x ∈ V ∧ A ⊆ No ∧ x ⊆ No ∧ ∀ y ∈ A ∀ z ∈ x y < s z ↔ ∀ y ∈ A y < s x
26 11 25 syl5bb ⊢ A ≪ s B ∧ x ∈ No → A ≪ s x ↔ ∀ y ∈ A y < s x
27 brsslt ⊢ x ≪ s B ↔ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
28 df-3an ⊢ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z ↔ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
29 28 bianass ⊢ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z ↔ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
30 27 29 bitri ⊢ x ≪ s B ↔ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
31 4 adantr ⊢ A ≪ s B ∧ x ∈ No → B ∈ V
32 31 13 jctil ⊢ A ≪ s B ∧ x ∈ No → x ∈ V ∧ B ∈ V
33 3 adantr ⊢ A ≪ s B ∧ x ∈ No → B ⊆ No
34 32 17 33 jca32 ⊢ A ≪ s B ∧ x ∈ No → x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No
35 34 biantrurd ⊢ A ≪ s B ∧ x ∈ No → ∀ y ∈ x ∀ z ∈ B y < s z ↔ x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z
36 35 bicomd ⊢ A ≪ s B ∧ x ∈ No → x ∈ V ∧ B ∈ V ∧ x ⊆ No ∧ B ⊆ No ∧ ∀ y ∈ x ∀ z ∈ B y < s z ↔ ∀ y ∈ x ∀ z ∈ B y < s z
37 30 36 syl5bb ⊢ A ≪ s B ∧ x ∈ No → x ≪ s B ↔ ∀ y ∈ x ∀ z ∈ B y < s z
38 breq1 ⊢ y = x → y < s z ↔ x < s z
39 38 ralbidv ⊢ y = x → ∀ z ∈ B y < s z ↔ ∀ z ∈ B x < s z
40 21 39 ralsn ⊢ ∀ y ∈ x ∀ z ∈ B y < s z ↔ ∀ z ∈ B x < s z
41 37 40 syl6bb ⊢ A ≪ s B ∧ x ∈ No → x ≪ s B ↔ ∀ z ∈ B x < s z
42 26 41 3anbi12d ⊢ A ≪ s B ∧ x ∈ No → A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B ↔ ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B
43 42 rexbidva ⊢ A ≪ s B → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B ↔ ∃ x ∈ No ∀ y ∈ A y < s x ∧ ∀ z ∈ B x < s z ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B
44 7 43 mpbird ⊢ A ≪ s B → ∃ x ∈ No A ≪ s x ∧ x ≪ s B ∧ bday ⁡ x ⊆ suc ⁡ ⋃ bday A ∪ B