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		intex	⊢ ( 𝐴 ≠ ∅ ↔ ∩ 𝐴 ∈ V )
43	42	bilani	⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ V )
44		iswun	⊢ ( ∩ 𝐴 ∈ V → ( ∩ 𝐴 ∈ WUni ↔ ( Tr ∩ 𝐴 ∧ ∩ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) ) ) )
45	43 44	syl	⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ( ∩ 𝐴 ∈ WUni ↔ ( Tr ∩ 𝐴 ∧ ∩ 𝐴 ≠ ∅ ∧ ∀ 𝑥 ∈ ∩ 𝐴 ( ∪ 𝑥 ∈ ∩ 𝐴 ∧ 𝒫 𝑥 ∈ ∩ 𝐴 ∧ ∀ 𝑦 ∈ ∩ 𝐴 { 𝑥 , 𝑦 } ∈ ∩ 𝐴 ) ) ) )
46	7 13 41 45	mpbir3and	⊢ ( ( 𝐴 ⊆ WUni ∧ 𝐴 ≠ ∅ ) → ∩ 𝐴 ∈ WUni )