This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem intwun

Description: The intersection of a collection of weak universes is a weak universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Assertion intwun ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ WUni )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → 𝐴 ⊆ WUni )
2 1 sselda ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ WUni )
3 wuntr ⊢ ( 𝑢 ∈ WUni → Tr 𝑢 )
4 2 3 syl ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑢 ∈ 𝐴 ) → Tr 𝑢 )
5 4 ralrimiva ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∀ 𝑢 ∈ 𝐴 Tr 𝑢 )
6 trint ⊢ ( ∀ 𝑢 ∈ 𝐴 Tr 𝑢 → Tr ∩ 𝐴 )
7 5 6 syl ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → Tr ∩ 𝐴 )
8 2 wun0 ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑢 ∈ 𝐴 ) → ∅ ∈ 𝑢 )
9 8 ralrimiva ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∀ 𝑢 ∈ 𝐴 ∅ ∈ 𝑢 )
10 0ex ⊢ ∅ ∈ V
11 10 elint2 ⊢ ( ∅ ∈ ∩ 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∅ ∈ 𝑢 )
12 9 11 sylibr ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∅ ∈ ∩ 𝐴 )
13 12 ne0d ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ≠ ∅ )
14 2 adantlr ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ WUni )
15 intss1 ⊢ ( 𝑢 ∈ 𝐴 → ∩ 𝐴 ⊆ 𝑢 )
16 15 adantl ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑢 ∈ 𝐴 ) → ∩ 𝐴 ⊆ 𝑢 )
17 16 sselda ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑥 ∈ ∩ 𝐴 ) → 𝑥 ∈ 𝑢 )
18 17 an32s ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝑥 ∈ 𝑢 )
19 14 18 wununi ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ∪ 𝑥 ∈ 𝑢 )
20 19 ralrimiva ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ∀ 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ 𝑢 )
21 vuniex ⊢ ∪ 𝑥 ∈ V
22 21 elint2 ⊢ ( ∪ 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 ∪ 𝑥 ∈ 𝑢 )
23 20 22 sylibr ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ∪ 𝑥 ∈ ∩ 𝐴 )
24 14 18 wunpw ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝒫 𝑥 ∈ 𝑢 )
25 24 ralrimiva ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ∀ 𝑢 ∈ 𝐴 𝒫 𝑥 ∈ 𝑢 )
26 vpwex ⊢ 𝒫 𝑥 ∈ V
27 26 elint2 ⊢ ( 𝒫 𝑥 ∈ ∩ 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 𝒫 𝑥 ∈ 𝑢 )
28 25 27 sylibr ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → 𝒫 𝑥 ∈ ∩ 𝐴 )
29 14 adantlr ⊢ ( ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝑢 ∈ WUni )
30 18 adantlr ⊢ ( ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝑥 ∈ 𝑢 )
31 15 adantl ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → ∩ 𝐴 ⊆ 𝑢 )
32 31 sselda ⊢ ( ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) → 𝑦 ∈ 𝑢 )
33 32 an32s ⊢ ( ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → 𝑦 ∈ 𝑢 )
34 29 30 33 wunpr ⊢ ( ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) ∧ 𝑢 ∈ 𝐴 ) → { 𝑥 , 𝑦 } ∈ 𝑢 )
35 34 ralrimiva ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) → ∀ 𝑢 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑢 )
36 prex ⊢ { 𝑥 , 𝑦 } ∈ V
37 36 elint2 ⊢ ( { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ↔ ∀ 𝑢 ∈ 𝐴 { 𝑥 , 𝑦 } ∈ 𝑢 )
38 35 37 sylibr ⊢ ( ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) ∧ 𝑦 ∈ ∩ 𝐴 ) → { 𝑥 , 𝑦 } ∈ ∩ 𝐴 )
39 38 ralrimiva ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 )
40 23 28 39 3jca ⊢ ( ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) ∧ 𝑥 ∈ ∩ 𝐴 ) → ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) )
41 40 ralrimiva ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∀ 𝑥 ∈ ∩ 𝐴 ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) )
42 simpr ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → 𝐴 ≠ ∅ )
43 intex ⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
44 42 43 sylib ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ V )
45 iswun ⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ WUni ↔ ( Tr ∩ 𝐴 ∧ ∩ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) ) ) )
46 44 45 syl ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ WUni ↔ ( Tr ∩ 𝐴 ∧ ∩ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) ) ) )
47 7 13 41 46 mpbir3and ⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ WUni )