Metamath Proof Explorer

Theorem unielss

Description: Two ways to say the union of a class is an element of a subclass. (Contributed by RP, 29-Jan-2025)

Ref Expression
Assertion unielss 
|- ( A C_ B -> ( U. B e. A <-> E. x e. A A. y e. B y C_ x ) )

Proof

Step Hyp Ref Expression
1 uniel 
 |-  ( U. B e. A <-> E. x e. A A. z ( z e. x <-> E. y e. B z e. y ) )
2 df-ss 
 |-  ( y C_ x <-> A. z ( z e. y -> z e. x ) )
3 2 ralbii 
 |-  ( A. y e. B y C_ x <-> A. y e. B A. z ( z e. y -> z e. x ) )
4 df-ral 
 |-  ( A. y e. B A. z ( z e. y -> z e. x ) <-> A. y ( y e. B -> A. z ( z e. y -> z e. x ) ) )
5 19.21v 
 |-  ( A. z ( y e. B -> ( z e. y -> z e. x ) ) <-> ( y e. B -> A. z ( z e. y -> z e. x ) ) )
6 5 albii 
 |-  ( A. y A. z ( y e. B -> ( z e. y -> z e. x ) ) <-> A. y ( y e. B -> A. z ( z e. y -> z e. x ) ) )
7 alcom 
 |-  ( A. y A. z ( y e. B -> ( z e. y -> z e. x ) ) <-> A. z A. y ( y e. B -> ( z e. y -> z e. x ) ) )
8 4 6 7 3bitr2i 
 |-  ( A. y e. B A. z ( z e. y -> z e. x ) <-> A. z A. y ( y e. B -> ( z e. y -> z e. x ) ) )
9 3 8 bitri 
 |-  ( A. y e. B y C_ x <-> A. z A. y ( y e. B -> ( z e. y -> z e. x ) ) )
10 ssel2 
 |-  ( ( A C_ B /\ x e. A ) -> x e. B )
11 pm2.27 
 |-  ( z e. x -> ( ( z e. x -> z e. x ) -> z e. x ) )
12 elequ2 
 |-  ( y = x -> ( z e. y <-> z e. x ) )
13 12 imbi1d 
 |-  ( y = x -> ( ( z e. y -> z e. x ) <-> ( z e. x -> z e. x ) ) )
14 13 12 imbi12d 
 |-  ( y = x -> ( ( ( z e. y -> z e. x ) -> z e. y ) <-> ( ( z e. x -> z e. x ) -> z e. x ) ) )
15 14 rspcev 
 |-  ( ( x e. B /\ ( ( z e. x -> z e. x ) -> z e. x ) ) -> E. y e. B ( ( z e. y -> z e. x ) -> z e. y ) )
16 10 11 15 syl2an 
 |-  ( ( ( A C_ B /\ x e. A ) /\ z e. x ) -> E. y e. B ( ( z e. y -> z e. x ) -> z e. y ) )
17 r19.35 
 |-  ( E. y e. B ( ( z e. y -> z e. x ) -> z e. y ) <-> ( A. y e. B ( z e. y -> z e. x ) -> E. y e. B z e. y ) )
18 df-ral 
 |-  ( A. y e. B ( z e. y -> z e. x ) <-> A. y ( y e. B -> ( z e. y -> z e. x ) ) )
19 18 imbi1i 
 |-  ( ( A. y e. B ( z e. y -> z e. x ) -> E. y e. B z e. y ) <-> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) -> E. y e. B z e. y ) )
20 17 19 bitri 
 |-  ( E. y e. B ( ( z e. y -> z e. x ) -> z e. y ) <-> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) -> E. y e. B z e. y ) )
21 16 20 sylib 
 |-  ( ( ( A C_ B /\ x e. A ) /\ z e. x ) -> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) -> E. y e. B z e. y ) )
22 21 impancom 
 |-  ( ( ( A C_ B /\ x e. A ) /\ A. y ( y e. B -> ( z e. y -> z e. x ) ) ) -> ( z e. x -> E. y e. B z e. y ) )
23 nfv 
 |-  F/ y ( A C_ B /\ x e. A )
24 nfa1 
 |-  F/ y A. y ( y e. B -> ( z e. y -> z e. x ) )
25 23 24 nfan 
 |-  F/ y ( ( A C_ B /\ x e. A ) /\ A. y ( y e. B -> ( z e. y -> z e. x ) ) )
26 nfv 
 |-  F/ y z e. x
27 sp 
 |-  ( A. y ( y e. B -> ( z e. y -> z e. x ) ) -> ( y e. B -> ( z e. y -> z e. x ) ) )
28 27 adantl 
 |-  ( ( ( A C_ B /\ x e. A ) /\ A. y ( y e. B -> ( z e. y -> z e. x ) ) ) -> ( y e. B -> ( z e. y -> z e. x ) ) )
29 25 26 28 rexlimd 
 |-  ( ( ( A C_ B /\ x e. A ) /\ A. y ( y e. B -> ( z e. y -> z e. x ) ) ) -> ( E. y e. B z e. y -> z e. x ) )
30 22 29 impbid 
 |-  ( ( ( A C_ B /\ x e. A ) /\ A. y ( y e. B -> ( z e. y -> z e. x ) ) ) -> ( z e. x <-> E. y e. B z e. y ) )
31 rspe 
 |-  ( ( y e. B /\ z e. y ) -> E. y e. B z e. y )
32 31 ex 
 |-  ( y e. B -> ( z e. y -> E. y e. B z e. y ) )
33 32 ax-gen 
 |-  A. y ( y e. B -> ( z e. y -> E. y e. B z e. y ) )
34 nfre1 
 |-  F/ y E. y e. B z e. y
35 26 34 nfbi 
 |-  F/ y ( z e. x <-> E. y e. B z e. y )
36 imbi2 
 |-  ( ( z e. x <-> E. y e. B z e. y ) -> ( ( z e. y -> z e. x ) <-> ( z e. y -> E. y e. B z e. y ) ) )
37 36 imbi2d 
 |-  ( ( z e. x <-> E. y e. B z e. y ) -> ( ( y e. B -> ( z e. y -> z e. x ) ) <-> ( y e. B -> ( z e. y -> E. y e. B z e. y ) ) ) )
38 35 37 albid 
 |-  ( ( z e. x <-> E. y e. B z e. y ) -> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) <-> A. y ( y e. B -> ( z e. y -> E. y e. B z e. y ) ) ) )
39 38 adantl 
 |-  ( ( ( A C_ B /\ x e. A ) /\ ( z e. x <-> E. y e. B z e. y ) ) -> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) <-> A. y ( y e. B -> ( z e. y -> E. y e. B z e. y ) ) ) )
40 33 39 mpbiri 
 |-  ( ( ( A C_ B /\ x e. A ) /\ ( z e. x <-> E. y e. B z e. y ) ) -> A. y ( y e. B -> ( z e. y -> z e. x ) ) )
41 30 40 impbida 
 |-  ( ( A C_ B /\ x e. A ) -> ( A. y ( y e. B -> ( z e. y -> z e. x ) ) <-> ( z e. x <-> E. y e. B z e. y ) ) )
42 41 albidv 
 |-  ( ( A C_ B /\ x e. A ) -> ( A. z A. y ( y e. B -> ( z e. y -> z e. x ) ) <-> A. z ( z e. x <-> E. y e. B z e. y ) ) )
43 9 42 bitrid 
 |-  ( ( A C_ B /\ x e. A ) -> ( A. y e. B y C_ x <-> A. z ( z e. x <-> E. y e. B z e. y ) ) )
44 43 rexbidva 
 |-  ( A C_ B -> ( E. x e. A A. y e. B y C_ x <-> E. x e. A A. z ( z e. x <-> E. y e. B z e. y ) ) )
45 1 44 bitr4id 
 |-  ( A C_ B -> ( U. B e. A <-> E. x e. A A. y e. B y C_ x ) )