Metamath Proof Explorer

Theorem ingru

Description: The intersection of a universe with a class that acts like a universe is another universe. (Contributed by Mario Carneiro, 10-Jun-2013)

Ref Expression
Assertion ingru ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∈ Univ → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )

Proof

Step Hyp Ref Expression
1 ineq1 ⊢ ( 𝑢 = 𝑈 → ( 𝑢 ∩ 𝐴 ) = ( 𝑈 ∩ 𝐴 ) )
2 1 eleq1d ⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 ∩ 𝐴 ) ∈ Univ ↔ ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )
3 2 imbi2d ⊢ ( 𝑢 = 𝑈 → ( ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑢 ∩ 𝐴 ) ∈ Univ ) ↔ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) ) )
4 elgrug ⊢ ( 𝑢 ∈ Univ → ( 𝑢 ∈ Univ ↔ ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) ) )
5 4 ibi ⊢ ( 𝑢 ∈ Univ → ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) )
6 trin ⊢ ( ( Tr 𝑢 ∧ Tr 𝐴 ) → Tr ( 𝑢 ∩ 𝐴 ) )
7 6 ex ⊢ ( Tr 𝑢 → ( Tr 𝐴 → Tr ( 𝑢 ∩ 𝐴 ) ) )
8 inss1 ⊢ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑢
9 ssralv ⊢ ( ( 𝑢 ∩ 𝐴 ) ⊆ 𝑢 → ( ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) )
10 8 9 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) )
11 inss2 ⊢ ( 𝑢 ∩ 𝐴 ) ⊆ 𝐴
12 ssralv ⊢ ( ( 𝑢 ∩ 𝐴 ) ⊆ 𝐴 → ( ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) )
13 11 12 ax-mp ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) )
14 elin ⊢ ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ↔ ( 𝒫 𝑥 ∈ 𝑢 ∧ 𝒫 𝑥 ∈ 𝐴 ) )
15 14 simplbi2 ⊢ ( 𝒫 𝑥 ∈ 𝑢 → ( 𝒫 𝑥 ∈ 𝐴 → 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ) )
16 ssralv ⊢ ( ( 𝑢 ∩ 𝐴 ) ⊆ 𝑢 → ( ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝑢 ) )
17 8 16 ax-mp ⊢ ( ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝑢 )
18 ssralv ⊢ ( ( 𝑢 ∩ 𝐴 ) ⊆ 𝐴 → ( ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝐴 ) )
19 11 18 ax-mp ⊢ ( ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝐴 )
20 elin ⊢ ( { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ↔ ( { 𝑥 , 𝑦 } ∈ 𝑢 ∧ { 𝑥 , 𝑦 } ∈ 𝐴 ) )
21 20 simplbi2 ⊢ ( { 𝑥 , 𝑦 } ∈ 𝑢 → ( { 𝑥 , 𝑦 } ∈ 𝐴 → { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) )
22 21 ral2imi ⊢ ( ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝑢 → ( ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ 𝐴 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) )
23 17 19 22 syl2im ⊢ ( ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 → ( ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 → ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) )
24 15 23 im2anan9 ⊢ ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) → ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) → ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
25 vex ⊢ 𝑢 ∈ V
26 mapss ⊢ ( ( 𝑢 ∈ V ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝑢 ) → ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ⊆ ( 𝑢 ↑m 𝑥 ) )
27 25 8 26 mp2an ⊢ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ⊆ ( 𝑢 ↑m 𝑥 )
28 ssralv ⊢ ( ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ⊆ ( 𝑢 ↑m 𝑥 ) → ( ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) )
29 27 28 ax-mp ⊢ ( ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 )
30 25 inex1 ⊢ ( 𝑢 ∩ 𝐴 ) ∈ V
31 vex ⊢ 𝑥 ∈ V
32 30 31 elmap ⊢ ( 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ↔ 𝑦 : 𝑥 ⟶ ( 𝑢 ∩ 𝐴 ) )
33 fss ⊢ ( ( 𝑦 : 𝑥 ⟶ ( 𝑢 ∩ 𝐴 ) ∧ ( 𝑢 ∩ 𝐴 ) ⊆ 𝐴 ) → 𝑦 : 𝑥 ⟶ 𝐴 )
34 11 33 mpan2 ⊢ ( 𝑦 : 𝑥 ⟶ ( 𝑢 ∩ 𝐴 ) → 𝑦 : 𝑥 ⟶ 𝐴 )
35 32 34 sylbi ⊢ ( 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) → 𝑦 : 𝑥 ⟶ 𝐴 )
36 35 imim1i ⊢ ( ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ( 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) → ∪ ran 𝑦 ∈ 𝐴 ) )
37 36 alimi ⊢ ( ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ( 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) → ∪ ran 𝑦 ∈ 𝐴 ) )
38 37 ralrid ⊢ ( ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝐴 )
39 elin ⊢ ( ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ↔ ( ∪ ran 𝑦 ∈ 𝑢 ∧ ∪ ran 𝑦 ∈ 𝐴 ) )
40 39 simplbi2 ⊢ ( ∪ ran 𝑦 ∈ 𝑢 → ( ∪ ran 𝑦 ∈ 𝐴 → ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
41 40 ral2imi ⊢ ( ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ( ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝐴 → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
42 29 38 41 syl2im ⊢ ( ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ( ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
43 24 42 im2anan9 ⊢ ( ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
44 43 3impa ⊢ ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
45 df-3an ⊢ ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ↔ ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) )
46 df-3an ⊢ ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ↔ ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
47 44 45 46 3imtr4g ⊢ ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
48 47 ral2imi ⊢ ( ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
49 10 13 48 syl2im ⊢ ( ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
50 7 49 im2anan9 ⊢ ( ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
51 5 50 syl ⊢ ( 𝑢 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
52 elgrug ⊢ ( ( 𝑢 ∩ 𝐴 ) ∈ V → ( ( 𝑢 ∩ 𝐴 ) ∈ Univ ↔ ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
53 30 52 ax-mp ⊢ ( ( 𝑢 ∩ 𝐴 ) ∈ Univ ↔ ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
54 51 53 imbitrrdi ⊢ ( 𝑢 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑢 ∩ 𝐴 ) ∈ Univ ) )
55 3 54 vtoclga ⊢ ( 𝑈 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )
56 55 com12 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∈ Univ → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )