Metamath Proof Explorer


Theorem nodense

Description: Given two distinct surreals with the same birthday, there is an older surreal lying between the two of them. Axiom SD of Alling p. 184. (Contributed by Scott Fenton, 16-Jun-2011)

Ref Expression
Assertion nodense ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 No ( ( bday 𝑥 ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s 𝑥𝑥 <s 𝐵 ) )

Proof

Step Hyp Ref Expression
1 nodenselem6 ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No )
2 bdayval ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No → ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) = dom ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
3 1 2 syl ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) = dom ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
4 dmres dom ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∩ dom 𝐴 )
5 nodenselem5 ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ ( bday 𝐴 ) )
6 bdayfo bday : No onto→ On
7 fof ( bday : No onto→ On → bday : No ⟶ On )
8 6 7 ax-mp bday : No ⟶ On
9 0elon ∅ ∈ On
10 8 9 f0cli ( bday 𝐴 ) ∈ On
11 10 onelssi ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ ( bday 𝐴 ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ ( bday 𝐴 ) )
12 5 11 syl ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ ( bday 𝐴 ) )
13 bdayval ( 𝐴 No → ( bday 𝐴 ) = dom 𝐴 )
14 13 ad2antrr ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday 𝐴 ) = dom 𝐴 )
15 12 14 sseqtrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ dom 𝐴 )
16 df-ss ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ⊆ dom 𝐴 ↔ ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∩ dom 𝐴 ) = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
17 15 16 sylib ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∩ dom 𝐴 ) = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
18 4 17 syl5eq ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → dom ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
19 3 18 eqtrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } )
20 19 5 eqeltrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ∈ ( bday 𝐴 ) )
21 nodenselem4 ( ( ( 𝐴 No 𝐵 No ) ∧ 𝐴 <s 𝐵 ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
22 21 adantrl ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On )
23 nodenselem8 ( ( 𝐴 No 𝐵 No ∧ ( bday 𝐴 ) = ( bday 𝐵 ) ) → ( 𝐴 <s 𝐵 ↔ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) )
24 23 biimpd ( ( 𝐴 No 𝐵 No ∧ ( bday 𝐴 ) = ( bday 𝐵 ) ) → ( 𝐴 <s 𝐵 → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) )
25 24 3expia ( ( 𝐴 No 𝐵 No ) → ( ( bday 𝐴 ) = ( bday 𝐵 ) → ( 𝐴 <s 𝐵 → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) ) )
26 25 imp32 ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) )
27 26 simpld ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o )
28 eqid ∅ = ∅
29 27 28 jctir ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ∅ = ∅ ) )
30 29 3mix1d ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ∅ = ∅ ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ∅ = 2o ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ∧ ∅ = 2o ) ) )
31 fvex ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ V
32 0ex ∅ ∈ V
33 31 32 brtp ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ ↔ ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ∅ = ∅ ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 1o ∧ ∅ = 2o ) ∨ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ∧ ∅ = 2o ) ) )
34 30 33 sylibr ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ∅ )
35 19 fveq2d ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
36 fvnobday ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) = ∅ )
37 1 36 syl ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) = ∅ )
38 35 37 eqtr3d ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ )
39 34 38 breqtrrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
40 fvres ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐴𝑦 ) )
41 40 eqcomd ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) )
42 41 rgen 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 )
43 39 42 jctil ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
44 raleq ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ↔ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ) )
45 fveq2 ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑥 ) = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
46 fveq2 ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
47 45 46 breq12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
48 44 47 anbi12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ) ↔ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
49 48 rspcev ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ) )
50 22 43 49 syl2anc ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ) )
51 simpll ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 No )
52 sltval ( ( 𝐴 No ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No ) → ( 𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ) ) )
53 51 1 52 syl2anc ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) ∧ ( 𝐴𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) ) ) )
54 50 53 mpbird ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
55 41 adantl ( ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝐴𝑦 ) = ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) )
56 nodenselem7 ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐴𝑦 ) = ( 𝐵𝑦 ) ) )
57 56 imp ( ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝐴𝑦 ) = ( 𝐵𝑦 ) )
58 55 57 eqtr3d ( ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) ∧ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) )
59 58 ralrimiva ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) )
60 26 simprd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o )
61 60 28 jctil ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ∅ = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) )
62 61 3mix3d ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( ∅ = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ) ∨ ( ∅ = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ∨ ( ∅ = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) )
63 fvex ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ V
64 32 63 brtp ( ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ↔ ( ( ∅ = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = ∅ ) ∨ ( ∅ = 1o ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ∨ ( ∅ = ∅ ∧ ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) = 2o ) ) )
65 62 64 sylibr ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∅ { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
66 38 65 eqbrtrd ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
67 raleq ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ↔ ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ) )
68 fveq2 ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( 𝐵𝑥 ) = ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) )
69 46 68 breq12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ↔ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
70 67 69 anbi12d ( 𝑥 = { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } → ( ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ↔ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) )
71 70 rspcev ( ( { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ∈ On ∧ ( ∀ 𝑦 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
72 22 59 66 71 syl12anc ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) )
73 simplr ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → 𝐵 No )
74 sltval ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No 𝐵 No ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
75 1 73 74 syl2anc ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 ↔ ∃ 𝑥 ∈ On ( ∀ 𝑦𝑥 ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑦 ) = ( 𝐵𝑦 ) ∧ ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ‘ 𝑥 ) { ⟨ 1o , ∅ ⟩ , ⟨ 1o , 2o ⟩ , ⟨ ∅ , 2o ⟩ } ( 𝐵𝑥 ) ) ) )
76 72 75 mpbird ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 )
77 fveq2 ( 𝑥 = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( bday 𝑥 ) = ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
78 77 eleq1d ( 𝑥 = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( ( bday 𝑥 ) ∈ ( bday 𝐴 ) ↔ ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ∈ ( bday 𝐴 ) ) )
79 breq2 ( 𝑥 = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝐴 <s 𝑥𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) )
80 breq1 ( 𝑥 = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( 𝑥 <s 𝐵 ↔ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 ) )
81 78 79 80 3anbi123d ( 𝑥 = ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) → ( ( ( bday 𝑥 ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s 𝑥𝑥 <s 𝐵 ) ↔ ( ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 ) ) )
82 81 rspcev ( ( ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∈ No ∧ ( ( bday ‘ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) ∧ ( 𝐴 { 𝑎 ∈ On ∣ ( 𝐴𝑎 ) ≠ ( 𝐵𝑎 ) } ) <s 𝐵 ) ) → ∃ 𝑥 No ( ( bday 𝑥 ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s 𝑥𝑥 <s 𝐵 ) )
83 1 20 54 76 82 syl13anc ( ( ( 𝐴 No 𝐵 No ) ∧ ( ( bday 𝐴 ) = ( bday 𝐵 ) ∧ 𝐴 <s 𝐵 ) ) → ∃ 𝑥 No ( ( bday 𝑥 ) ∈ ( bday 𝐴 ) ∧ 𝐴 <s 𝑥𝑥 <s 𝐵 ) )