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 ( 𝑎 𝑇 𝑏 ↔ ( ( 𝐹𝑎 ) 𝑅 ( 𝐹𝑏 ) ∨ ( ( 𝐹𝑎 ) = ( 𝐹𝑏 ) ∧ 𝑎 ( 𝐹𝑎 ) / 𝑧 𝑆 𝑏 ) ) )