Metamath Proof Explorer


Theorem weiunlem1

Description: Lemma for weiunpo , weiunso , weiunfr , and weiunse . (Contributed by Matthew House, 8-Sep-2025)

Ref Expression
Hypotheses weiun.1 F = w x A B ι u x A | w B | v x A | w B ¬ v R u
weiun.2 T = y z | y x A B z x A B F y R F z F y = F z y F y / x S z
Assertion weiunlem1 C T D C x A B D x A B F C R F D F C = F D C F C / x S D

Proof

Step Hyp Ref Expression
1 weiun.1 F = w x A B ι u x A | w B | v x A | w B ¬ v R u
2 weiun.2 T = y z | y x A B z x A B F y R F z F y = F z y F y / x S z
3 simpl y = C z = D y = C
4 3 fveq2d y = C z = D F y = F C
5 simpr y = C z = D z = D
6 5 fveq2d y = C z = D F z = F D
7 4 6 breq12d y = C z = D F y R F z F C R F D
8 4 6 eqeq12d y = C z = D F y = F z F C = F D
9 4 csbeq1d y = C z = D F y / x S = F C / x S
10 3 9 5 breq123d y = C z = D y F y / x S z C F C / x S D
11 8 10 anbi12d y = C z = D F y = F z y F y / x S z F C = F D C F C / x S D
12 7 11 orbi12d y = C z = D F y R F z F y = F z y F y / x S z F C R F D F C = F D C F C / x S D
13 12 2 brab2a C T D C x A B D x A B F C R F D F C = F D C F C / x S D