This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fnwe2lem1

Description: Lemma for fnwe2 . Substitution in well-ordering hypothesis. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
fnwe2.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
fnwe2.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
Assertion fnwe2lem1 ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } )

Proof

Step Hyp Ref Expression
1 fnwe2.su ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
2 fnwe2.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3 fnwe2.s ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
4 3 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
5 fveq2 ⊢ ( 𝑎 = 𝑥 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑥 ) )
6 5 csbeq1d ⊢ ( 𝑎 = 𝑥 → ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 )
7 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
8 7 1 csbie ⊢ ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 = 𝑈
9 6 8 eqtrdi ⊢ ( 𝑎 = 𝑥 → ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 = 𝑈 )
10 5 eqeq2d ⊢ ( 𝑎 = 𝑥 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ) )
11 10 rabbidv ⊢ ( 𝑎 = 𝑥 → { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } = { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
12 9 11 weeq12d ⊢ ( 𝑎 = 𝑥 → ( ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } ↔ 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } ) )
13 12 cbvralvw ⊢ ( ∀ 𝑎 ∈ 𝐴 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } ↔ ∀ 𝑥 ∈ 𝐴 𝑈 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) } )
14 4 13 sylibr ⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } )
15 14 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 We { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } )