Metamath Proof Explorer

Theorem refun0

Description: Adding the empty set preserves refinements. (Contributed by Thierry Arnoux, 31-Jan-2020)

Ref Expression
Assertion refun0 
|- ( ( A Ref B /\ B =/= (/) ) -> ( A u. { (/) } ) Ref B )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  U. A = U. A
2 eqid 
 |-  U. B = U. B
3 1 2 refbas 
 |-  ( A Ref B -> U. B = U. A )
4 3 adantr 
 |-  ( ( A Ref B /\ B =/= (/) ) -> U. B = U. A )
5 elun 
 |-  ( x e. ( A u. { (/) } ) <-> ( x e. A \/ x e. { (/) } ) )
6 refssex 
 |-  ( ( A Ref B /\ x e. A ) -> E. y e. B x C_ y )
7 6 adantlr 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ x e. A ) -> E. y e. B x C_ y )
8 0ss 
 |-  (/) C_ y
9 8 a1i 
 |-  ( ( A Ref B /\ y e. B ) -> (/) C_ y )
10 9 reximdva0 
 |-  ( ( A Ref B /\ B =/= (/) ) -> E. y e. B (/) C_ y )
11 10 adantr 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ x e. { (/) } ) -> E. y e. B (/) C_ y )
12 elsni 
 |-  ( x e. { (/) } -> x = (/) )
13 sseq1 
 |-  ( x = (/) -> ( x C_ y <-> (/) C_ y ) )
14 13 rexbidv 
 |-  ( x = (/) -> ( E. y e. B x C_ y <-> E. y e. B (/) C_ y ) )
15 12 14 syl 
 |-  ( x e. { (/) } -> ( E. y e. B x C_ y <-> E. y e. B (/) C_ y ) )
16 15 adantl 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ x e. { (/) } ) -> ( E. y e. B x C_ y <-> E. y e. B (/) C_ y ) )
17 11 16 mpbird 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ x e. { (/) } ) -> E. y e. B x C_ y )
18 7 17 jaodan 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ ( x e. A \/ x e. { (/) } ) ) -> E. y e. B x C_ y )
19 5 18 sylan2b 
 |-  ( ( ( A Ref B /\ B =/= (/) ) /\ x e. ( A u. { (/) } ) ) -> E. y e. B x C_ y )
20 19 ralrimiva 
 |-  ( ( A Ref B /\ B =/= (/) ) -> A. x e. ( A u. { (/) } ) E. y e. B x C_ y )
21 refrel 
 |-  Rel Ref
22 21 brrelex1i 
 |-  ( A Ref B -> A e. _V )
23 p0ex 
 |-  { (/) } e. _V
24 unexg 
 |-  ( ( A e. _V /\ { (/) } e. _V ) -> ( A u. { (/) } ) e. _V )
25 22 23 24 sylancl 
 |-  ( A Ref B -> ( A u. { (/) } ) e. _V )
26 uniun 
 |-  U. ( A u. { (/) } ) = ( U. A u. U. { (/) } )
27 0ex 
 |-  (/) e. _V
28 27 unisn 
 |-  U. { (/) } = (/)
29 28 uneq2i 
 |-  ( U. A u. U. { (/) } ) = ( U. A u. (/) )
30 un0 
 |-  ( U. A u. (/) ) = U. A
31 26 29 30 3eqtrri 
 |-  U. A = U. ( A u. { (/) } )
32 31 2 isref 
 |-  ( ( A u. { (/) } ) e. _V -> ( ( A u. { (/) } ) Ref B <-> ( U. B = U. A /\ A. x e. ( A u. { (/) } ) E. y e. B x C_ y ) ) )
33 25 32 syl 
 |-  ( A Ref B -> ( ( A u. { (/) } ) Ref B <-> ( U. B = U. A /\ A. x e. ( A u. { (/) } ) E. y e. B x C_ y ) ) )
34 33 adantr 
 |-  ( ( A Ref B /\ B =/= (/) ) -> ( ( A u. { (/) } ) Ref B <-> ( U. B = U. A /\ A. x e. ( A u. { (/) } ) E. y e. B x C_ y ) ) )
35 4 20 34 mpbir2and 
 |-  ( ( A Ref B /\ B =/= (/) ) -> ( A u. { (/) } ) Ref B )