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

Metamath Proof Explorer

Theorem satf0suclem

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

Ref Expression
Assertion satf0suclem 
|- ( ( X e. U /\ Y e. V /\ Z e. W ) -> { <. x , y >. | ( y = (/) /\ E. u e. X ( E. v e. Y x = B \/ E. w e. Z x = C ) ) } e. _V )

Proof

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