Metamath Proof Explorer

Theorem noetainflem2

Description: Lemma for noeta . The restriction of W to the domain of T is T . (Contributed by Scott Fenton, 9-Aug-2024)

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

Proof

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