Theorem djuexb

Description: The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023)

	Ref	Expression
Assertion	djuexb	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ⊔ 𝐵 ) ∈ V )

Proof

Step	Hyp	Ref	Expression
1		djuex	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )
2		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
3	2	eleq1i	⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
4		unexb	⊢ ( ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
5	3 4	bitr4i	⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V ↔ ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) )
6		0nep0	⊢ ∅ ≠ { ∅ }
7	6	necomi	⊢ { ∅ } ≠ ∅
8		rnexg	⊢ ( ( { ∅ } × 𝐴 ) ∈ V → ran ( { ∅ } × 𝐴 ) ∈ V )
9		rnxp	⊢ ( { ∅ } ≠ ∅ → ran ( { ∅ } × 𝐴 ) = 𝐴 )
10	9	eleq1d	⊢ ( { ∅ } ≠ ∅ → ( ran ( { ∅ } × 𝐴 ) ∈ V ↔ 𝐴 ∈ V ) )
11	8 10	imbitrid	⊢ ( { ∅ } ≠ ∅ → ( ( { ∅ } × 𝐴 ) ∈ V → 𝐴 ∈ V ) )
12	7 11	ax-mp	⊢ ( ( { ∅ } × 𝐴 ) ∈ V → 𝐴 ∈ V )
13		1oex	⊢ 1o ∈ V
14	13	snnz	⊢ { 1o } ≠ ∅
15		rnexg	⊢ ( ( { 1o } × 𝐵 ) ∈ V → ran ( { 1o } × 𝐵 ) ∈ V )
16		rnxp	⊢ ( { 1o } ≠ ∅ → ran ( { 1o } × 𝐵 ) = 𝐵 )
17	16	eleq1d	⊢ ( { 1o } ≠ ∅ → ( ran ( { 1o } × 𝐵 ) ∈ V ↔ 𝐵 ∈ V ) )
18	15 17	imbitrid	⊢ ( { 1o } ≠ ∅ → ( ( { 1o } × 𝐵 ) ∈ V → 𝐵 ∈ V ) )
19	14 18	ax-mp	⊢ ( ( { 1o } × 𝐵 ) ∈ V → 𝐵 ∈ V )
20	12 19	anim12i	⊢ ( ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
21	5 20	sylbi	⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
22	1 21	impbii	⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ⊔ 𝐵 ) ∈ V )