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 df-ral ⊢ ( ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝐴 ↔ ∀ 𝑦 ( 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) → ∪ ran 𝑦 ∈ 𝐴 ) )
39 37 38 sylibr ⊢ ( ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝐴 )
40 elin ⊢ ( ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ↔ ( ∪ ran 𝑦 ∈ 𝑢 ∧ ∪ ran 𝑦 ∈ 𝐴 ) )
41 40 simplbi2 ⊢ ( ∪ ran 𝑦 ∈ 𝑢 → ( ∪ ran 𝑦 ∈ 𝐴 → ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
42 41 ral2imi ⊢ ( ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ( ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝐴 → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
43 29 39 42 syl2im ⊢ ( ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 → ( ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) → ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
44 24 43 im2anan9 ⊢ ( ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
45 44 3impa ⊢ ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
46 df-3an ⊢ ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ↔ ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ) ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) )
47 df-3an ⊢ ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ↔ ( ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) )
48 45 46 47 3imtr4g ⊢ ( ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
49 48 ral2imi ⊢ ( ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
50 10 13 49 syl2im ⊢ ( ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) → ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
51 7 50 im2anan9 ⊢ ( ( Tr 𝑢 ∧ ∀ 𝑥 ∈ 𝑢 ( 𝒫 𝑥 ∈ 𝑢 ∧ ∀ 𝑦 ∈ 𝑢 { 𝑥 , 𝑦 } ∈ 𝑢 ∧ ∀ 𝑦 ∈ ( 𝑢 ↑m 𝑥 ) ∪ ran 𝑦 ∈ 𝑢 ) ) → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
52 5 51 syl ⊢ ( 𝑢 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
53 elgrug ⊢ ( ( 𝑢 ∩ 𝐴 ) ∈ V → ( ( 𝑢 ∩ 𝐴 ) ∈ Univ ↔ ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) ) )
54 30 53 ax-mp ⊢ ( ( 𝑢 ∩ 𝐴 ) ∈ Univ ↔ ( Tr ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ( 𝒫 𝑥 ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) { 𝑥 , 𝑦 } ∈ ( 𝑢 ∩ 𝐴 ) ∧ ∀ 𝑦 ∈ ( ( 𝑢 ∩ 𝐴 ) ↑m 𝑥 ) ∪ ran 𝑦 ∈ ( 𝑢 ∩ 𝐴 ) ) ) )
55 52 54 syl6ibr ⊢ ( 𝑢 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑢 ∩ 𝐴 ) ∈ Univ ) )
56 3 55 vtoclga ⊢ ( 𝑈 ∈ Univ → ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )
57 56 com12 ⊢ ( ( Tr 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝒫 𝑥 ∈ 𝐴 ∧ ∀ 𝑦 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝐴 ∧ ∀ 𝑦 ( 𝑦 : 𝑥 ⟶ 𝐴 → ∪ ran 𝑦 ∈ 𝐴 ) ) ) → ( 𝑈 ∈ Univ → ( 𝑈 ∩ 𝐴 ) ∈ Univ ) )