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 { 𝑦 ∈ 𝐴 ∣ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑎 ) } )