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 < E. x e. No ( A <

Proof

Step Hyp Ref Expression
1 ssltss1 
 |-  ( A < A C_ No )
2 ssltex1 
 |-  ( A < A e. _V )
3 1 2 jca 
 |-  ( A < ( A C_ No /\ A e. _V ) )
4 ssltss2 
 |-  ( A < B C_ No )
5 ssltex2 
 |-  ( A < B e. _V )
6 4 5 jca 
 |-  ( A < ( B C_ No /\ B e. _V ) )
7 ssltsep 
 |-  ( A < A. y e. A A. z e. B y
8 3 6 7 3jca 
 |-  ( A < ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. y e. A A. z e. B y
9 8 3ad2ant1 
 |-  ( ( A < ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. y e. A A. z e. B y
10 3simpc 
 |-  ( ( A < ( O e. On /\ ( bday " ( A u. B ) ) C_ O ) )
11 noeta 
 |-  ( ( ( ( A C_ No /\ A e. _V ) /\ ( B C_ No /\ B e. _V ) /\ A. y e. A A. z e. B y  E. x e. No ( A. y e. A y
12 9 10 11 syl2anc 
 |-  ( ( A < E. x e. No ( A. y e. A y
13 2 ad2antrr 
 |-  ( ( ( A < A e. _V )
14 snex 
 |-  { x } e. _V
15 13 14 jctir 
 |-  ( ( ( A < ( A e. _V /\ { x } e. _V ) )
16 1 ad2antrr 
 |-  ( ( ( A < A C_ No )
17 snssi 
 |-  ( x e. No -> { x } C_ No )
18 17 ad2antrl 
 |-  ( ( ( A < { x } C_ No )
19 simprr1 
 |-  ( ( ( A < A. y e. A y
20 vex 
 |-  x e. _V
21 breq2 
 |-  ( z = x -> ( y  y
22 20 21 ralsn 
 |-  ( A. z e. { x } y  y
23 22 ralbii 
 |-  ( A. y e. A A. z e. { x } y  A. y e. A y
24 19 23 sylibr 
 |-  ( ( ( A < A. y e. A A. z e. { x } y
25 16 18 24 3jca 
 |-  ( ( ( A < ( A C_ No /\ { x } C_ No /\ A. y e. A A. z e. { x } y
26 brsslt 
 |-  ( A < ( ( A e. _V /\ { x } e. _V ) /\ ( A C_ No /\ { x } C_ No /\ A. y e. A A. z e. { x } y
27 15 25 26 sylanbrc 
 |-  ( ( ( A < A <
28 5 ad2antrr 
 |-  ( ( ( A < B e. _V )
29 28 14 jctil 
 |-  ( ( ( A < ( { x } e. _V /\ B e. _V ) )
30 4 ad2antrr 
 |-  ( ( ( A < B C_ No )
31 simprr2 
 |-  ( ( ( A < A. z e. B x
32 breq1 
 |-  ( y = x -> ( y  x
33 32 ralbidv 
 |-  ( y = x -> ( A. z e. B y  A. z e. B x
34 20 33 ralsn 
 |-  ( A. y e. { x } A. z e. B y  A. z e. B x
35 31 34 sylibr 
 |-  ( ( ( A < A. y e. { x } A. z e. B y
36 18 30 35 3jca 
 |-  ( ( ( A < ( { x } C_ No /\ B C_ No /\ A. y e. { x } A. z e. B y
37 brsslt 
 |-  ( { x } < ( ( { x } e. _V /\ B e. _V ) /\ ( { x } C_ No /\ B C_ No /\ A. y e. { x } A. z e. B y
38 29 36 37 sylanbrc 
 |-  ( ( ( A < { x } <
39 simprr3 
 |-  ( ( ( A < ( bday ` x ) C_ O )
40 27 38 39 3jca 
 |-  ( ( ( A < ( A <
41 40 expr 
 |-  ( ( ( A < ( ( A. y e. A y  ( A <
42 41 reximdva 
 |-  ( ( A < ( E. x e. No ( A. y e. A y  E. x e. No ( A <
43 42 3adant3 
 |-  ( ( A < ( E. x e. No ( A. y e. A y  E. x e. No ( A <
44 12 43 mpd 
 |-  ( ( A < E. x e. No ( A <