Metamath Proof Explorer

Theorem etasslt

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

Ref Expression
Assertion etasslt ⊢A≪sB∧O∈On∧bdayA∪B⊆O→∃x∈NoA≪sx∧x≪sB∧bday⁡x⊆O

Proof

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