Theorem grupr

Description: A Grothendieck universe contains pairs derived from its elements. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	grupr	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		elgrug	⊢ ( 𝑈 ∈ Univ → ( 𝑈 ∈ Univ ↔ ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) ) )
2	1	ibi	⊢ ( 𝑈 ∈ Univ → ( Tr 𝑈 ∧ ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) ) )
3	2	simprd	⊢ ( 𝑈 ∈ Univ → ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) )
4		preq2	⊢ ( 𝑦 = 𝐵 → { 𝑥 , 𝑦 } = { 𝑥 , 𝐵 } )
5	4	eleq1d	⊢ ( 𝑦 = 𝐵 → ( { 𝑥 , 𝑦 } ∈ 𝑈 ↔ { 𝑥 , 𝐵 } ∈ 𝑈 ) )
6	5	rspccv	⊢ ( ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 → ( 𝐵 ∈ 𝑈 → { 𝑥 , 𝐵 } ∈ 𝑈 ) )
7	6	3ad2ant2	⊢ ( ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) → ( 𝐵 ∈ 𝑈 → { 𝑥 , 𝐵 } ∈ 𝑈 ) )
8	7	com12	⊢ ( 𝐵 ∈ 𝑈 → ( ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) → { 𝑥 , 𝐵 } ∈ 𝑈 ) )
9	8	ralimdv	⊢ ( 𝐵 ∈ 𝑈 → ( ∀ 𝑥 ∈ 𝑈 ( 𝒫 𝑥 ∈ 𝑈 ∧ ∀ 𝑦 ∈ 𝑈 { 𝑥 , 𝑦 } ∈ 𝑈 ∧ ∀ 𝑦 ∈ ( 𝑈 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝑈 { 𝑥 , 𝐵 } ∈ 𝑈 ) )
10	3 9	syl5com	⊢ ( 𝑈 ∈ Univ → ( 𝐵 ∈ 𝑈 → ∀ 𝑥 ∈ 𝑈 { 𝑥 , 𝐵 } ∈ 𝑈 ) )
11		preq1	⊢ ( 𝑥 = 𝐴 → { 𝑥 , 𝐵 } = { 𝐴 , 𝐵 } )
12	11	eleq1d	⊢ ( 𝑥 = 𝐴 → ( { 𝑥 , 𝐵 } ∈ 𝑈 ↔ { 𝐴 , 𝐵 } ∈ 𝑈 ) )
13	12	rspccv	⊢ ( ∀ 𝑥 ∈ 𝑈 { 𝑥 , 𝐵 } ∈ 𝑈 → ( 𝐴 ∈ 𝑈 → { 𝐴 , 𝐵 } ∈ 𝑈 ) )
14	10 13	syl6	⊢ ( 𝑈 ∈ Univ → ( 𝐵 ∈ 𝑈 → ( 𝐴 ∈ 𝑈 → { 𝐴 , 𝐵 } ∈ 𝑈 ) ) )
15	14	com23	⊢ ( 𝑈 ∈ Univ → ( 𝐴 ∈ 𝑈 → ( 𝐵 ∈ 𝑈 → { 𝐴 , 𝐵 } ∈ 𝑈 ) ) )
16	15	3imp	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑈 ) → { 𝐴 , 𝐵 } ∈ 𝑈 )