Metamath Proof Explorer

Theorem noextenddif

Description: Calculate the place where a surreal and its extension differ. (Contributed by Scott Fenton, 22-Nov-2021)

Ref Expression
Hypothesis noextend.1 ⊢ 𝑋 ∈ { 1o , 2o }
Assertion noextenddif ( 𝐴 ∈ No → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } = dom 𝐴 )

Proof

Step Hyp Ref Expression
1 noextend.1 ⊢ 𝑋 ∈ { 1o , 2o }
2 nodmon ⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ On )
3 1 nosgnn0i ⊢ ∅ ≠ 𝑋
4 3 a1i ⊢ ( 𝐴 ∈ No → ∅ ≠ 𝑋 )
5 nodmord ⊢ ( 𝐴 ∈ No → Ord dom 𝐴 )
6 ordirr ⊢ ( Ord dom 𝐴 → ¬ dom 𝐴 ∈ dom 𝐴 )
7 5 6 syl ⊢ ( 𝐴 ∈ No → ¬ dom 𝐴 ∈ dom 𝐴 )
8 ndmfv ⊢ ( ¬ dom 𝐴 ∈ dom 𝐴 → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
9 7 8 syl ⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) = ∅ )
10 nofun ⊢ ( 𝐴 ∈ No → Fun 𝐴 )
11 funfn ⊢ ( Fun 𝐴 ↔ 𝐴 Fn dom 𝐴 )
12 10 11 sylib ⊢ ( 𝐴 ∈ No → 𝐴 Fn dom 𝐴 )
13 fnsng ⊢ ( ( dom 𝐴 ∈ On ∧ 𝑋 ∈ { 1o , 2o } ) → { ⟨ dom 𝐴 , 𝑋 ⟩ } Fn { dom 𝐴 } )
14 2 1 13 sylancl ⊢ ( 𝐴 ∈ No → { ⟨ dom 𝐴 , 𝑋 ⟩ } Fn { dom 𝐴 } )
15 disjsn ⊢ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ↔ ¬ dom 𝐴 ∈ dom 𝐴 )
16 7 15 sylibr ⊢ ( 𝐴 ∈ No → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ )
17 snidg ⊢ ( dom 𝐴 ∈ On → dom 𝐴 ∈ { dom 𝐴 } )
18 2 17 syl ⊢ ( 𝐴 ∈ No → dom 𝐴 ∈ { dom 𝐴 } )
19 fvun2 ⊢ ( ( 𝐴 Fn dom 𝐴 ∧ { ⟨ dom 𝐴 , 𝑋 ⟩ } Fn { dom 𝐴 } ∧ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ∧ dom 𝐴 ∈ { dom 𝐴 } ) ) → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) = ( { ⟨ dom 𝐴 , 𝑋 ⟩ } ‘ dom 𝐴 ) )
20 12 14 16 18 19 syl112anc ⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) = ( { ⟨ dom 𝐴 , 𝑋 ⟩ } ‘ dom 𝐴 ) )
21 fvsng ⊢ ( ( dom 𝐴 ∈ On ∧ 𝑋 ∈ { 1o , 2o } ) → ( { ⟨ dom 𝐴 , 𝑋 ⟩ } ‘ dom 𝐴 ) = 𝑋 )
22 2 1 21 sylancl ⊢ ( 𝐴 ∈ No → ( { ⟨ dom 𝐴 , 𝑋 ⟩ } ‘ dom 𝐴 ) = 𝑋 )
23 20 22 eqtrd ⊢ ( 𝐴 ∈ No → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) = 𝑋 )
24 4 9 23 3netr4d ⊢ ( 𝐴 ∈ No → ( 𝐴 ‘ dom 𝐴 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) )
25 fveq2 ⊢ ( 𝑥 = dom 𝐴 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ dom 𝐴 ) )
26 fveq2 ⊢ ( 𝑥 = dom 𝐴 → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) )
27 25 26 neeq12d ⊢ ( 𝑥 = dom 𝐴 → ( ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ dom 𝐴 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) ) )
28 27 onintss ⊢ ( dom 𝐴 ∈ On → ( ( 𝐴 ‘ dom 𝐴 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ dom 𝐴 ) → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } ⊆ dom 𝐴 ) )
29 2 24 28 sylc ⊢ ( 𝐴 ∈ No → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } ⊆ dom 𝐴 )
30 eloni ⊢ ( 𝑦 ∈ On → Ord 𝑦 )
31 ordtri2 ⊢ ( ( Ord 𝑦 ∧ Ord dom 𝐴 ) → ( 𝑦 ∈ dom 𝐴 ↔ ¬ ( 𝑦 = dom 𝐴 ∨ dom 𝐴 ∈ 𝑦 ) ) )
32 eqcom ⊢ ( 𝑦 = dom 𝐴 ↔ dom 𝐴 = 𝑦 )
33 32 orbi1i ⊢ ( ( 𝑦 = dom 𝐴 ∨ dom 𝐴 ∈ 𝑦 ) ↔ ( dom 𝐴 = 𝑦 ∨ dom 𝐴 ∈ 𝑦 ) )
34 orcom ⊢ ( ( dom 𝐴 = 𝑦 ∨ dom 𝐴 ∈ 𝑦 ) ↔ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) )
35 33 34 bitri ⊢ ( ( 𝑦 = dom 𝐴 ∨ dom 𝐴 ∈ 𝑦 ) ↔ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) )
36 35 notbii ⊢ ( ¬ ( 𝑦 = dom 𝐴 ∨ dom 𝐴 ∈ 𝑦 ) ↔ ¬ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) )
37 31 36 bitrdi ⊢ ( ( Ord 𝑦 ∧ Ord dom 𝐴 ) → ( 𝑦 ∈ dom 𝐴 ↔ ¬ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) ) )
38 ordsseleq ⊢ ( ( Ord dom 𝐴 ∧ Ord 𝑦 ) → ( dom 𝐴 ⊆ 𝑦 ↔ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) ) )
39 38 notbid ⊢ ( ( Ord dom 𝐴 ∧ Ord 𝑦 ) → ( ¬ dom 𝐴 ⊆ 𝑦 ↔ ¬ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) ) )
40 39 ancoms ⊢ ( ( Ord 𝑦 ∧ Ord dom 𝐴 ) → ( ¬ dom 𝐴 ⊆ 𝑦 ↔ ¬ ( dom 𝐴 ∈ 𝑦 ∨ dom 𝐴 = 𝑦 ) ) )
41 37 40 bitr4d ⊢ ( ( Ord 𝑦 ∧ Ord dom 𝐴 ) → ( 𝑦 ∈ dom 𝐴 ↔ ¬ dom 𝐴 ⊆ 𝑦 ) )
42 30 5 41 syl2anr ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ dom 𝐴 ↔ ¬ dom 𝐴 ⊆ 𝑦 ) )
43 12 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → 𝐴 Fn dom 𝐴 )
44 14 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → { ⟨ dom 𝐴 , 𝑋 ⟩ } Fn { dom 𝐴 } )
45 16 3ad2ant1 ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ )
46 simp3 ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → 𝑦 ∈ dom 𝐴 )
47 fvun1 ⊢ ( ( 𝐴 Fn dom 𝐴 ∧ { ⟨ dom 𝐴 , 𝑋 ⟩ } Fn { dom 𝐴 } ∧ ( ( dom 𝐴 ∩ { dom 𝐴 } ) = ∅ ∧ 𝑦 ∈ dom 𝐴 ) ) → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
48 43 44 45 46 47 syl112anc ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) = ( 𝐴 ‘ 𝑦 ) )
49 48 eqcomd ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ∧ 𝑦 ∈ dom 𝐴 ) → ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) )
50 49 3expia ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ) → ( 𝑦 ∈ dom 𝐴 → ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) ) )
51 42 50 sylbird ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ) → ( ¬ dom 𝐴 ⊆ 𝑦 → ( 𝐴 ‘ 𝑦 ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) ) )
52 51 necon1ad ⊢ ( ( 𝐴 ∈ No ∧ 𝑦 ∈ On ) → ( ( 𝐴 ‘ 𝑦 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) → dom 𝐴 ⊆ 𝑦 ) )
53 52 ralrimiva ⊢ ( 𝐴 ∈ No → ∀ 𝑦 ∈ On ( ( 𝐴 ‘ 𝑦 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) → dom 𝐴 ⊆ 𝑦 ) )
54 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ‘ 𝑥 ) = ( 𝐴 ‘ 𝑦 ) )
55 fveq2 ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) = ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) )
56 54 55 neeq12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) ↔ ( 𝐴 ‘ 𝑦 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) ) )
57 56 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } dom 𝐴 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ On ( ( 𝐴 ‘ 𝑦 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑦 ) → dom 𝐴 ⊆ 𝑦 ) )
58 53 57 sylibr ⊢ ( 𝐴 ∈ No → ∀ 𝑦 ∈ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } dom 𝐴 ⊆ 𝑦 )
59 ssint ⊢ ( dom 𝐴 ⊆ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } dom 𝐴 ⊆ 𝑦 )
60 58 59 sylibr ⊢ ( 𝐴 ∈ No → dom 𝐴 ⊆ ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } )
61 29 60 eqssd ⊢ ( 𝐴 ∈ No → ∩ { 𝑥 ∈ On ∣ ( 𝐴 ‘ 𝑥 ) ≠ ( ( 𝐴 ∪ { ⟨ dom 𝐴 , 𝑋 ⟩ } ) ‘ 𝑥 ) } = dom 𝐴 )