Metamath Proof Explorer

Theorem refun0

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

Ref Expression
Assertion refun0 ⊢ARefB∧B≠∅→A∪∅RefB

Proof

Step Hyp Ref Expression
1 eqid ⊢⋃A=⋃A
2 eqid ⊢⋃B=⋃B
3 1 2 refbas ⊢ARefB→⋃B=⋃A
4 3 adantr ⊢ARefB∧B≠∅→⋃B=⋃A
5 elun ⊢x∈A∪∅↔x∈A∨x∈∅
6 refssex ⊢ARefB∧x∈A→∃y∈Bx⊆y
7 6 adantlr ⊢ARefB∧B≠∅∧x∈A→∃y∈Bx⊆y
8 0ss ⊢∅⊆y
9 8 a1i ⊢ARefB∧y∈B→∅⊆y
10 9 reximdva0 ⊢ARefB∧B≠∅→∃y∈B∅⊆y
11 10 adantr ⊢ARefB∧B≠∅∧x∈∅→∃y∈B∅⊆y
12 elsni ⊢x∈∅→x=∅
13 sseq1 ⊢x=∅→x⊆y↔∅⊆y
14 13 rexbidv ⊢x=∅→∃y∈Bx⊆y↔∃y∈B∅⊆y
15 12 14 syl ⊢x∈∅→∃y∈Bx⊆y↔∃y∈B∅⊆y
16 15 adantl ⊢ARefB∧B≠∅∧x∈∅→∃y∈Bx⊆y↔∃y∈B∅⊆y
17 11 16 mpbird ⊢ARefB∧B≠∅∧x∈∅→∃y∈Bx⊆y
18 7 17 jaodan ⊢ARefB∧B≠∅∧x∈A∨x∈∅→∃y∈Bx⊆y
19 5 18 sylan2b ⊢ARefB∧B≠∅∧x∈A∪∅→∃y∈Bx⊆y
20 19 ralrimiva ⊢ARefB∧B≠∅→∀x∈A∪∅∃y∈Bx⊆y
21 refrel ⊢Rel⁡Ref
22 21 brrelex1i ⊢ARefB→A∈V
23 p0ex ⊢∅∈V
24 unexg ⊢A∈V∧∅∈V→A∪∅∈V
25 22 23 24 sylancl ⊢ARefB→A∪∅∈V
26 uniun ⊢⋃A∪∅=⋃A∪⋃∅
27 0ex ⊢∅∈V
28 27 unisn ⊢⋃∅=∅
29 28 uneq2i ⊢⋃A∪⋃∅=⋃A∪∅
30 un0 ⊢⋃A∪∅=⋃A
31 26 29 30 3eqtrri ⊢⋃A=⋃A∪∅
32 31 2 isref ⊢A∪∅∈V→A∪∅RefB↔⋃B=⋃A∧∀x∈A∪∅∃y∈Bx⊆y
33 25 32 syl ⊢ARefB→A∪∅RefB↔⋃B=⋃A∧∀x∈A∪∅∃y∈Bx⊆y
34 33 adantr ⊢ARefB∧B≠∅→A∪∅RefB↔⋃B=⋃A∧∀x∈A∪∅∃y∈Bx⊆y
35 4 20 34 mpbir2and ⊢ARefB∧B≠∅→A∪∅RefB