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 6 7 syl ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → Fun 𝑇 )
9 funrel ⊢ ( Fun 𝑇 → Rel 𝑇 )
10 resdm ⊢ ( Rel 𝑇 → ( 𝑇 ↾ dom 𝑇 ) = 𝑇 )
11 8 9 10 3syl ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( 𝑇 ↾ dom 𝑇 ) = 𝑇 )
12 dmres ⊢ dom ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ( dom 𝑇 ∩ dom ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) )
13 2oex ⊢ 2o ∈ V
14 13 snnz ⊢ { 2o } ≠ ∅
15 dmxp ⊢ ( { 2o } ≠ ∅ → dom ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) = ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) )
16 14 15 ax-mp ⊢ dom ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) = ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 )
17 16 ineq2i ⊢ ( dom 𝑇 ∩ dom ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ) = ( dom 𝑇 ∩ ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) )
18 disjdif ⊢ ( dom 𝑇 ∩ ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) ) = ∅
19 17 18 eqtri ⊢ ( dom 𝑇 ∩ dom ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ) = ∅
20 12 19 eqtri ⊢ dom ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅
21 relres ⊢ Rel ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 )
22 reldm0 ⊢ ( Rel ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) → ( ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅ ↔ dom ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅ ) )
23 21 22 ax-mp ⊢ ( ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅ ↔ dom ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅ )
24 20 23 mpbir ⊢ ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅
25 24 a1i ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) = ∅ )
26 11 25 uneq12d ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( ( 𝑇 ↾ dom 𝑇 ) ∪ ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) ) = ( 𝑇 ∪ ∅ ) )
27 un0 ⊢ ( 𝑇 ∪ ∅ ) = 𝑇
28 26 27 eqtrdi ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( ( 𝑇 ↾ dom 𝑇 ) ∪ ( ( ( suc ∪ ( bday “ 𝐴 ) ∖ dom 𝑇 ) × { 2o } ) ↾ dom 𝑇 ) ) = 𝑇 )
29 5 28 syl5eq ⊢ ( ( 𝐵 ⊆ No ∧ 𝐵 ∈ V ) → ( 𝑊 ↾ dom 𝑇 ) = 𝑇 )