Metamath Proof Explorer

Theorem wunfi

Description: A weak universe contains all finite sets with elements drawn from the universe. (Contributed by Mario Carneiro, 2-Jan-2017)

Ref Expression
Hypotheses wun0.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
wunfi.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
wunfi.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
Assertion wunfi ( 𝜑 → 𝐴 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 wun0.1 ⊢ ( 𝜑 → 𝑈 ∈ WUni )
2 wunfi.2 ⊢ ( 𝜑 → 𝐴 ⊆ 𝑈 )
3 wunfi.3 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
4 sseq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ⊆ 𝑈 ↔ ∅ ⊆ 𝑈 ) )
5 eleq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 ∈ 𝑈 ↔ ∅ ∈ 𝑈 ) )
6 4 5 imbi12d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ↔ ( ∅ ⊆ 𝑈 → ∅ ∈ 𝑈 ) ) )
7 6 imbi2d ⊢ ( 𝑥 = ∅ → ( ( 𝜑 → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) ↔ ( 𝜑 → ( ∅ ⊆ 𝑈 → ∅ ∈ 𝑈 ) ) ) )
8 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝑈 ↔ 𝑦 ⊆ 𝑈 ) )
9 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑈 ↔ 𝑦 ∈ 𝑈 ) )
10 8 9 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ↔ ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) ) )
11 10 imbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) ↔ ( 𝜑 → ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) ) ) )
12 sseq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ⊆ 𝑈 ↔ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ) )
13 eleq1 ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( 𝑥 ∈ 𝑈 ↔ ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) )
14 12 13 imbi12d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ↔ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) )
15 14 imbi2d ⊢ ( 𝑥 = ( 𝑦 ∪ { 𝑧 } ) → ( ( 𝜑 → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) ↔ ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) ) )
16 sseq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ⊆ 𝑈 ↔ 𝐴 ⊆ 𝑈 ) )
17 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝑈 ↔ 𝐴 ∈ 𝑈 ) )
18 16 17 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ↔ ( 𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈 ) ) )
19 18 imbi2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝜑 → ( 𝑥 ⊆ 𝑈 → 𝑥 ∈ 𝑈 ) ) ↔ ( 𝜑 → ( 𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈 ) ) ) )
20 1 wun0 ⊢ ( 𝜑 → ∅ ∈ 𝑈 )
21 20 a1d ⊢ ( 𝜑 → ( ∅ ⊆ 𝑈 → ∅ ∈ 𝑈 ) )
22 ssun1 ⊢ 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } )
23 sstr ⊢ ( ( 𝑦 ⊆ ( 𝑦 ∪ { 𝑧 } ) ∧ ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ) → 𝑦 ⊆ 𝑈 )
24 22 23 mpan ⊢ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → 𝑦 ⊆ 𝑈 )
25 24 imim1i ⊢ ( ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) )
26 1 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑈 ∈ WUni )
27 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑦 ∈ 𝑈 )
28 simprl ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 )
29 28 unssbd ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → { 𝑧 } ⊆ 𝑈 )
30 vex ⊢ 𝑧 ∈ V
31 30 snss ⊢ ( 𝑧 ∈ 𝑈 ↔ { 𝑧 } ⊆ 𝑈 )
32 29 31 sylibr ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → 𝑧 ∈ 𝑈 )
33 26 32 wunsn ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → { 𝑧 } ∈ 𝑈 )
34 26 27 33 wunun ⊢ ( ( 𝜑 ∧ ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 ∧ 𝑦 ∈ 𝑈 ) ) → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 )
35 34 exp32 ⊢ ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∈ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) )
36 35 a2d ⊢ ( 𝜑 → ( ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) )
37 25 36 syl5 ⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) )
38 37 a2i ⊢ ( ( 𝜑 → ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) )
39 38 a1i ⊢ ( 𝑦 ∈ Fin → ( ( 𝜑 → ( 𝑦 ⊆ 𝑈 → 𝑦 ∈ 𝑈 ) ) → ( 𝜑 → ( ( 𝑦 ∪ { 𝑧 } ) ⊆ 𝑈 → ( 𝑦 ∪ { 𝑧 } ) ∈ 𝑈 ) ) ) )
40 7 11 15 19 21 39 findcard2 ⊢ ( 𝐴 ∈ Fin → ( 𝜑 → ( 𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈 ) ) )
41 3 40 mpcom ⊢ ( 𝜑 → ( 𝐴 ⊆ 𝑈 → 𝐴 ∈ 𝑈 ) )
42 2 41 mpd ⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )