Metamath Proof Explorer


Theorem nogesgn1o

Description: Given A greater than or equal to B , equal to B up to X , and A ( X ) = 1o , then B ( X ) = 1o . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Assertion nogesgn1o ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐵𝑋 ) = 1o )

Proof

Step Hyp Ref Expression
1 simpl2 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → 𝐵 No )
2 nofv ( 𝐵 No → ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 1o ∨ ( 𝐵𝑋 ) = 2o ) )
3 1 2 syl ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 1o ∨ ( 𝐵𝑋 ) = 2o ) )
4 3orel2 ( ¬ ( 𝐵𝑋 ) = 1o → ( ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 1o ∨ ( 𝐵𝑋 ) = 2o ) → ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) )
5 3 4 syl5com ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → ( ¬ ( 𝐵𝑋 ) = 1o → ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) )
6 simp13 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → 𝑋 ∈ On )
7 fveq1 ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) → ( ( 𝐴𝑋 ) ‘ 𝑦 ) = ( ( 𝐵𝑋 ) ‘ 𝑦 ) )
8 7 adantr ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝐴𝑋 ) ‘ 𝑦 ) = ( ( 𝐵𝑋 ) ‘ 𝑦 ) )
9 simpr ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ 𝑦𝑋 ) → 𝑦𝑋 )
10 9 fvresd ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝐴𝑋 ) ‘ 𝑦 ) = ( 𝐴𝑦 ) )
11 9 fvresd ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ 𝑦𝑋 ) → ( ( 𝐵𝑋 ) ‘ 𝑦 ) = ( 𝐵𝑦 ) )
12 8 10 11 3eqtr3d ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ 𝑦𝑋 ) → ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
13 12 ralrimiva ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) → ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
14 13 adantr ( ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) → ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
15 14 3ad2ant2 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
16 simp2r ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( 𝐴𝑋 ) = 1o )
17 simp3 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) )
18 16 17 jca ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( ( 𝐴𝑋 ) = 1o ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) )
19 andi ( ( ( 𝐴𝑋 ) = 1o ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) ↔ ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ) )
20 18 19 sylib ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ) )
21 3mix1 ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) → ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ∨ ( ( 𝐴𝑋 ) = ∅ ∧ ( 𝐵𝑋 ) = 2o ) ) )
22 3mix2 ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) → ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ∨ ( ( 𝐴𝑋 ) = ∅ ∧ ( 𝐵𝑋 ) = 2o ) ) )
23 21 22 jaoi ( ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ) → ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ∨ ( ( 𝐴𝑋 ) = ∅ ∧ ( 𝐵𝑋 ) = 2o ) ) )
24 20 23 syl ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ∨ ( ( 𝐴𝑋 ) = ∅ ∧ ( 𝐵𝑋 ) = 2o ) ) )
25 fvex ( 𝐴𝑋 ) ∈ V
26 fvex ( 𝐵𝑋 ) ∈ V
27 25 26 brtp ( ( 𝐴𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑋 ) ↔ ( ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = ∅ ) ∨ ( ( 𝐴𝑋 ) = 1o ∧ ( 𝐵𝑋 ) = 2o ) ∨ ( ( 𝐴𝑋 ) = ∅ ∧ ( 𝐵𝑋 ) = 2o ) ) )
28 24 27 sylibr ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( 𝐴𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑋 ) )
29 raleq ( 𝑥 = 𝑋 → ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ↔ ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) )
30 fveq2 ( 𝑥 = 𝑋 → ( 𝐴𝑥 ) = ( 𝐴𝑋 ) )
31 fveq2 ( 𝑥 = 𝑋 → ( 𝐵𝑥 ) = ( 𝐵𝑋 ) )
32 30 31 breq12d ( 𝑥 = 𝑋 → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ↔ ( 𝐴𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑋 ) ) )
33 29 32 anbi12d ( 𝑥 = 𝑋 → ( ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ↔ ( ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑋 ) ) ) )
34 33 rspcev ( ( 𝑋 ∈ On ∧ ( ∀ 𝑦𝑋 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑋 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑋 ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
35 6 15 28 34 syl12anc ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
36 simp11 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → 𝐴 No )
37 simp12 ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → 𝐵 No )
38 sltval ( ( 𝐴 No 𝐵 No ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
39 36 37 38 syl2anc ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → ( 𝐴 <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
40 35 39 mpbird ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) ) → 𝐴 <s 𝐵 )
41 40 3expia ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → ( ( ( 𝐵𝑋 ) = ∅ ∨ ( 𝐵𝑋 ) = 2o ) → 𝐴 <s 𝐵 ) )
42 5 41 syld ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → ( ¬ ( 𝐵𝑋 ) = 1o𝐴 <s 𝐵 ) )
43 42 con1d ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ) → ( ¬ 𝐴 <s 𝐵 → ( 𝐵𝑋 ) = 1o ) )
44 43 3impia ( ( ( 𝐴 No 𝐵 No 𝑋 ∈ On ) ∧ ( ( 𝐴𝑋 ) = ( 𝐵𝑋 ) ∧ ( 𝐴𝑋 ) = 1o ) ∧ ¬ 𝐴 <s 𝐵 ) → ( 𝐵𝑋 ) = 1o )