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

Metamath Proof Explorer

Theorem refun0

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

Ref Expression
Assertion refun0 ( ( 𝐴 Ref 𝐵 ∧ 𝐵 ≠ ∅ ) → ( 𝐴 ∪ { ∅ } ) Ref 𝐵 )

Proof

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