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

Metamath Proof Explorer

Theorem fnwe2val

Description: Lemma for fnwe2 . Substitute variables. (Contributed by Stefan O'Rear, 19-Jan-2015)

Ref Expression
Hypotheses fnwe2.su ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
fnwe2.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
Assertion fnwe2val ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 fnwe2.su ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑥 ) → 𝑆 = 𝑈 )
2 fnwe2.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) }
3 vex ⊢ 𝑎 ∈ V
4 vex ⊢ 𝑏 ∈ V
5 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
6 fveq2 ⊢ ( 𝑦 = 𝑏 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑏 ) )
7 5 6 breqan12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ) )
8 5 6 eqeqan12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ) )
9 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
10 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
11 10 1 csbie ⊢ ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 = 𝑈
12 5 csbeq1d ⊢ ( 𝑥 = 𝑎 → ⦋ ( 𝐹 ‘ 𝑥 ) / 𝑧 ⦌ 𝑆 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
13 11 12 eqtr3id ⊢ ( 𝑥 = 𝑎 → 𝑈 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
14 13 adantr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑈 = ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 )
15 simpr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑦 = 𝑏 )
16 9 14 15 breq123d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 𝑈 𝑦 ↔ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) )
17 8 16 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )
18 7 17 orbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 𝐹 ‘ 𝑥 ) 𝑅 ( 𝐹 ‘ 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 𝑈 𝑦 ) ) ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) ) )
19 3 4 18 2 braba ⊢ ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹 ‘ 𝑎 ) 𝑅 ( 𝐹 ‘ 𝑏 ) ∨ ( ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑏 ) ∧ 𝑎 ⦋ ( 𝐹 ‘ 𝑎 ) / 𝑧 ⦌ 𝑆 𝑏 ) ) )