Metamath Proof Explorer

Theorem noetasuplem2

Description: Lemma for noeta . The restriction of Z to dom S is S . (Contributed by Scott Fenton, 9-Aug-2024)

Ref Expression
Hypotheses noetasuplem.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
noetasuplem.2 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
Assertion noetasuplem2 ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )

Proof

Step Hyp Ref Expression
1 noetasuplem.1 ⊢ 𝑆 = if ( ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 , ( ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) ∪ { ⟨ dom ( ℩ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 <s 𝑦 ) , 2o ⟩ } ) , ( 𝑔 ∈ { 𝑦 ∣ ∃ 𝑢 ∈ 𝐴 ( 𝑦 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑦 ) = ( 𝑣 ↾ suc 𝑦 ) ) ) } ↦ ( ℩ 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝑔 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑣 <s 𝑢 → ( 𝑢 ↾ suc 𝑔 ) = ( 𝑣 ↾ suc 𝑔 ) ) ∧ ( 𝑢 ‘ 𝑔 ) = 𝑥 ) ) ) )
2 noetasuplem.2 ⊢ 𝑍 = ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
3 2 reseq1i ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 )
4 resundir ⊢ ( ( 𝑆 ∪ ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) ↾ dom 𝑆 ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) )
5 dmres ⊢ dom ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ( dom 𝑆 ∩ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) )
6 1oex ⊢ 1o ∈ V
7 6 snnz ⊢ { 1o } ≠ ∅
8 dmxp ⊢ ( { 1o } ≠ ∅ → dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) = ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
9 7 8 ax-mp ⊢ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) = ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 )
10 9 ineq2i ⊢ ( dom 𝑆 ∩ dom ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ) = ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) )
11 disjdif ⊢ ( dom 𝑆 ∩ ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) ) = ∅
12 5 10 11 3eqtri ⊢ dom ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
13 relres ⊢ Rel ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 )
14 reldm0 ⊢ ( Rel ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) → ( ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅ ↔ dom ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅ ) )
15 13 14 ax-mp ⊢ ( ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅ ↔ dom ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅ )
16 12 15 mpbir ⊢ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) = ∅
17 16 uneq2i ⊢ ( ( 𝑆 ↾ dom 𝑆 ) ∪ ( ( ( suc ∪ ( bday “ 𝐵 ) ∖ dom 𝑆 ) × { 1o } ) ↾ dom 𝑆 ) ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
18 3 4 17 3eqtri ⊢ ( 𝑍 ↾ dom 𝑆 ) = ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ )
19 1 nosupno ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ) → 𝑆 ∈ No )
20 19 3adant3 ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → 𝑆 ∈ No )
21 nofun ⊢ ( 𝑆 ∈ No → Fun 𝑆 )
22 20 21 syl ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → Fun 𝑆 )
23 funrel ⊢ ( Fun 𝑆 → Rel 𝑆 )
24 resdm ⊢ ( Rel 𝑆 → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
25 22 23 24 3syl ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑆 ↾ dom 𝑆 ) = 𝑆 )
26 25 uneq1d ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = ( 𝑆 ∪ ∅ ) )
27 un0 ⊢ ( 𝑆 ∪ ∅ ) = 𝑆
28 26 27 eqtrdi ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( ( 𝑆 ↾ dom 𝑆 ) ∪ ∅ ) = 𝑆 )
29 18 28 syl5eq ⊢ ( ( 𝐴 ⊆ No ∧ 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝑍 ↾ dom 𝑆 ) = 𝑆 )