Theorem prct

Description: An unordered pair is countable. (Contributed by Thierry Arnoux, 16-Sep-2016)

	Ref	Expression
Assertion	prct	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 , 𝐵 } ≼ ω )

Proof

Step	Hyp	Ref	Expression
1		df-pr	⊢ { 𝐴 , 𝐵 } = ( { 𝐴 } ∪ { 𝐵 } )
2		snct	⊢ ( 𝐴 ∈ 𝑉 → { 𝐴 } ≼ ω )
3		snct	⊢ ( 𝐵 ∈ 𝑊 → { 𝐵 } ≼ ω )
4		unctb	⊢ ( ( { 𝐴 } ≼ ω ∧ { 𝐵 } ≼ ω ) → ( { 𝐴 } ∪ { 𝐵 } ) ≼ ω )
5	2 3 4	syl2an	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 𝐴 } ∪ { 𝐵 } ) ≼ ω )
6	1 5	eqbrtrid	⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → { 𝐴 , 𝐵 } ≼ ω )