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 ∪ ∅ Ref B

Proof

Step Hyp Ref Expression
1 eqid ⊢ ⋃ A = ⋃ A
2 eqid ⊢ ⋃ B = ⋃ B
3 1 2 refbas ⊢ A Ref B → ⋃ B = ⋃ A
4 3 adantr ⊢ A Ref B ∧ B ≠ ∅ → ⋃ B = ⋃ A
5 elun ⊢ x ∈ A ∪ ∅ ↔ x ∈ A ∨ x ∈ ∅
6 refssex ⊢ A Ref B ∧ x ∈ A → ∃ y ∈ B x ⊆ y
7 6 adantlr ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ A → ∃ y ∈ B x ⊆ y
8 0ss ⊢ ∅ ⊆ y
9 8 a1i ⊢ A Ref B ∧ y ∈ B → ∅ ⊆ y
10 9 reximdva0 ⊢ A Ref B ∧ B ≠ ∅ → ∃ y ∈ B ∅ ⊆ y
11 10 adantr ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ ∅ → ∃ y ∈ B ∅ ⊆ y
12 elsni ⊢ x ∈ ∅ → x = ∅
13 sseq1 ⊢ x = ∅ → x ⊆ y ↔ ∅ ⊆ y
14 13 rexbidv ⊢ x = ∅ → ∃ y ∈ B x ⊆ y ↔ ∃ y ∈ B ∅ ⊆ y
15 12 14 syl ⊢ x ∈ ∅ → ∃ y ∈ B x ⊆ y ↔ ∃ y ∈ B ∅ ⊆ y
16 15 adantl ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ ∅ → ∃ y ∈ B x ⊆ y ↔ ∃ y ∈ B ∅ ⊆ y
17 11 16 mpbird ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ ∅ → ∃ y ∈ B x ⊆ y
18 7 17 jaodan ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ A ∨ x ∈ ∅ → ∃ y ∈ B x ⊆ y
19 5 18 sylan2b ⊢ A Ref B ∧ B ≠ ∅ ∧ x ∈ A ∪ ∅ → ∃ y ∈ B x ⊆ y
20 19 ralrimiva ⊢ A Ref B ∧ B ≠ ∅ → ∀ x ∈ A ∪ ∅ ∃ y ∈ B x ⊆ y
21 refrel ⊢ Rel ⁡ Ref
22 21 brrelex1i ⊢ A Ref B → A ∈ V
23 p0ex ⊢ ∅ ∈ V
24 unexg ⊢ A ∈ V ∧ ∅ ∈ V → A ∪ ∅ ∈ V
25 22 23 24 sylancl ⊢ A Ref B → 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 ∪ ∅ Ref B ↔ ⋃ B = ⋃ A ∧ ∀ x ∈ A ∪ ∅ ∃ y ∈ B x ⊆ y
33 25 32 syl ⊢ A Ref B → A ∪ ∅ Ref B ↔ ⋃ B = ⋃ A ∧ ∀ x ∈ A ∪ ∅ ∃ y ∈ B x ⊆ y
34 33 adantr ⊢ A Ref B ∧ B ≠ ∅ → A ∪ ∅ Ref B ↔ ⋃ B = ⋃ A ∧ ∀ x ∈ A ∪ ∅ ∃ y ∈ B x ⊆ y
35 4 20 34 mpbir2and ⊢ A Ref B ∧ B ≠ ∅ → A ∪ ∅ Ref B