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 𝐵 )