Theorem wunpr

Description: A weak universe is closed under pairing. (Contributed by Mario Carneiro, 2-Jan-2017)

	Ref	Expression
Hypotheses	wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
	wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	wunpr.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
Assertion	wunpr	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		wununi.1	⊢ ( 𝜑 → 𝑈 ∈ WUni )
2		wununi.2	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
3		wunpr.3	⊢ ( 𝜑 → 𝐵 ∈ 𝑈 )
4		iswun	⊢ ( 𝑈 ∈ WUni → ( 𝑈 ∈ WUni ↔ ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) ) )
5	4	ibi	⊢ ( 𝑈 ∈ WUni → ( Tr 𝑈 ∧ 𝑈 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) ) )
6	5	simp3d	⊢ ( 𝑈 ∈ WUni → ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) )
7		simp3	⊢ ( ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
8	7	ralimi	⊢ ( ∀ 𝑥 ∈ 𝑈 ( ∪ 𝑥 ∈ 𝑈 ∧ 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
9	1 6 8	3syl	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 )
10		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝑦 } = { 𝐴 , 𝑦 } )
11	10	eleq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 , 𝑦 } ∈ 𝑈 ↔ { 𝐴 , 𝑦 } ∈ 𝑈 ) )
12		preq2	⊢ ( 𝑦 = 𝐵 → { 𝐴 , 𝑦 } = { 𝐴 , 𝐵 } )
13	12	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝐴 , 𝑦 } ∈ 𝑈 ↔ { 𝐴 , 𝐵 } ∈ 𝑈 ) )
14	11 13	rspc2va	⊢ ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) ∧ ∀ 𝑥 ∈ 𝑈 ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )
15	2 3 9 14	syl21anc	⊢ ( 𝜑 → { 𝐴 , 𝐵 } ∈ 𝑈 )