Metamath Proof Explorer

Theorem resslemOLD

Description: Obsolete version of resseqnbas as of 21-Oct-2024. (Contributed by Mario Carneiro, 26-Nov-2014) (Revised by Mario Carneiro, 2-Dec-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses resslemOLD.r ⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
resslemOLD.e ⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
resslemOLD.f ⊢ 𝐸 = Slot 𝑁
resslemOLD.n ⊢ 𝑁 ∈ ℕ
resslemOLD.b ⊢ 1 < 𝑁
Assertion resslemOLD ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 resslemOLD.r ⊢ 𝑅 = ( 𝑊 ↾s 𝐴 )
2 resslemOLD.e ⊢ 𝐶 = ( 𝐸 ‘ 𝑊 )
3 resslemOLD.f ⊢ 𝐸 = Slot 𝑁
4 resslemOLD.n ⊢ 𝑁 ∈ ℕ
5 resslemOLD.b ⊢ 1 < 𝑁
6 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
7 1 6 ressid2 ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = 𝑊 )
8 7 fveq2d ⊢ ( ( ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
9 8 3expib ⊢ ( ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
10 1 6 ressval2 ⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → 𝑅 = ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
11 10 fveq2d ⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) ) )
12 3 4 ndxid ⊢ 𝐸 = Slot ( 𝐸 ‘ ndx )
13 3 4 ndxarg ⊢ ( 𝐸 ‘ ndx ) = 𝑁
14 1re ⊢ 1 ∈ ℝ
15 14 5 gtneii ⊢ 𝑁 ≠ 1
16 13 15 eqnetri ⊢ ( 𝐸 ‘ ndx ) ≠ 1
17 basendx ⊢ ( Base ‘ ndx ) = 1
18 16 17 neeqtrri ⊢ ( 𝐸 ‘ ndx ) ≠ ( Base ‘ ndx )
19 12 18 setsnid ⊢ ( 𝐸 ‘ 𝑊 ) = ( 𝐸 ‘ ( 𝑊 sSet ⟨ ( Base ‘ ndx ) , ( 𝐴 ∩ ( Base ‘ 𝑊 ) ) ⟩ ) )
20 11 19 eqtr4di ⊢ ( ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 ∧ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
21 20 3expib ⊢ ( ¬ ( Base ‘ 𝑊 ) ⊆ 𝐴 → ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) ) )
22 9 21 pm2.61i ⊢ ( ( 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
23 reldmress ⊢ Rel dom ↾s
24 23 ovprc1 ⊢ ( ¬ 𝑊 ∈ V → ( 𝑊 ↾s 𝐴 ) = ∅ )
25 1 24 eqtrid ⊢ ( ¬ 𝑊 ∈ V → 𝑅 = ∅ )
26 25 fveq2d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ ∅ ) )
27 3 str0 ⊢ ∅ = ( 𝐸 ‘ ∅ )
28 26 27 eqtr4di ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ∅ )
29 fvprc ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑊 ) = ∅ )
30 28 29 eqtr4d ⊢ ( ¬ 𝑊 ∈ V → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
31 30 adantr ⊢ ( ( ¬ 𝑊 ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
32 22 31 pm2.61ian ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐸 ‘ 𝑅 ) = ( 𝐸 ‘ 𝑊 ) )
33 2 32 eqtr4id ⊢ ( 𝐴 ∈ 𝑉 → 𝐶 = ( 𝐸 ‘ 𝑅 ) )