Metamath Proof Explorer


Theorem satf0suclem

Description: Lemma for satf0suc , sat1el2xp and fmlasuc0 . (Contributed by AV, 19-Sep-2023)

Ref Expression
Assertion satf0suclem X U Y V Z W x y | y = u X v Y x = B w Z x = C V

Proof

Step Hyp Ref Expression
1 peano1 ω
2 eleq1 y = y ω ω
3 1 2 mpbiri y = y ω
4 3 adantr y = u X v Y x = B w Z x = C y ω
5 4 pm4.71ri y = u X v Y x = B w Z x = C y ω y = u X v Y x = B w Z x = C
6 5 opabbii x y | y = u X v Y x = B w Z x = C = x y | y ω y = u X v Y x = B w Z x = C
7 omex ω V
8 7 a1i X U Y V Z W ω V
9 simp1 X U Y V Z W X U
10 unab x | v Y x = B x | w Z x = C = x | v Y x = B w Z x = C
11 abrexexg Y V x | v Y x = B V
12 11 3ad2ant2 X U Y V Z W x | v Y x = B V
13 abrexexg Z W x | w Z x = C V
14 13 3ad2ant3 X U Y V Z W x | w Z x = C V
15 unexg x | v Y x = B V x | w Z x = C V x | v Y x = B x | w Z x = C V
16 12 14 15 syl2anc X U Y V Z W x | v Y x = B x | w Z x = C V
17 10 16 eqeltrrid X U Y V Z W x | v Y x = B w Z x = C V
18 17 ralrimivw X U Y V Z W u X x | v Y x = B w Z x = C V
19 abrexex2g X U u X x | v Y x = B w Z x = C V x | u X v Y x = B w Z x = C V
20 9 18 19 syl2anc X U Y V Z W x | u X v Y x = B w Z x = C V
21 20 adantr X U Y V Z W y ω x | u X v Y x = B w Z x = C V
22 8 21 opabex3rd X U Y V Z W x y | y ω u X v Y x = B w Z x = C V
23 simpr y = u X v Y x = B w Z x = C u X v Y x = B w Z x = C
24 23 anim2i y ω y = u X v Y x = B w Z x = C y ω u X v Y x = B w Z x = C
25 24 ssopab2i x y | y ω y = u X v Y x = B w Z x = C x y | y ω u X v Y x = B w Z x = C
26 25 a1i X U Y V Z W x y | y ω y = u X v Y x = B w Z x = C x y | y ω u X v Y x = B w Z x = C
27 22 26 ssexd X U Y V Z W x y | y ω y = u X v Y x = B w Z x = C V
28 6 27 eqeltrid X U Y V Z W x y | y = u X v Y x = B w Z x = C V