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	$⊢ φ \to U \in WUni$
	wunfi.2	$⊢ φ \to A \subseteq U$
	wunfi.3	$⊢ φ \to A \in Fin$
Assertion	wunfi	$⊢ φ \to A \in U$

Proof

Step	Hyp	Ref	Expression
1		wun0.1	$⊢ φ \to U \in WUni$
2		wunfi.2	$⊢ φ \to A \subseteq U$
3		wunfi.3	$⊢ φ \to A \in Fin$
4		sseq1	$⊢ x = \emptyset \to (x \subseteq U \leftrightarrow \emptyset \subseteq U)$
5		eleq1	$⊢ x = \emptyset \to (x \in U \leftrightarrow \emptyset \in U)$
6	4 5	imbi12d	$⊢ x = \emptyset \to ((x \subseteq U \to x \in U) \leftrightarrow (\emptyset \subseteq U \to \emptyset \in U))$
7	6	imbi2d	$⊢ x = \emptyset \to ((φ \to (x \subseteq U \to x \in U)) \leftrightarrow (φ \to (\emptyset \subseteq U \to \emptyset \in U)))$
8		sseq1	$⊢ x = y \to (x \subseteq U \leftrightarrow y \subseteq U)$
9		eleq1	$⊢ x = y \to (x \in U \leftrightarrow y \in U)$
10	8 9	imbi12d	$⊢ x = y \to ((x \subseteq U \to x \in U) \leftrightarrow (y \subseteq U \to y \in U))$
11	10	imbi2d	$⊢ x = y \to ((φ \to (x \subseteq U \to x \in U)) \leftrightarrow (φ \to (y \subseteq U \to y \in U)))$
12		sseq1	$⊢ x = y \cup \{z\} \to (x \subseteq U \leftrightarrow y \cup \{z\} \subseteq U)$
13		eleq1	$⊢ x = y \cup \{z\} \to (x \in U \leftrightarrow y \cup \{z\} \in U)$
14	12 13	imbi12d	$⊢ x = y \cup \{z\} \to ((x \subseteq U \to x \in U) \leftrightarrow (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U))$
15	14	imbi2d	$⊢ x = y \cup \{z\} \to ((φ \to (x \subseteq U \to x \in U)) \leftrightarrow (φ \to (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U)))$
16		sseq1	$⊢ x = A \to (x \subseteq U \leftrightarrow A \subseteq U)$
17		eleq1	$⊢ x = A \to (x \in U \leftrightarrow A \in U)$
18	16 17	imbi12d	$⊢ x = A \to ((x \subseteq U \to x \in U) \leftrightarrow (A \subseteq U \to A \in U))$
19	18	imbi2d	$⊢ x = A \to ((φ \to (x \subseteq U \to x \in U)) \leftrightarrow (φ \to (A \subseteq U \to A \in U)))$
20	1	wun0	$⊢ φ \to \emptyset \in U$
21	20	a1d	$⊢ φ \to (\emptyset \subseteq U \to \emptyset \in U)$
22		ssun1	$⊢ y \subseteq y \cup \{z\}$
23		sstr	$⊢ (y \subseteq y \cup \{z\} \land y \cup \{z\} \subseteq U) \to y \subseteq U$
24	22 23	mpan	$⊢ y \cup \{z\} \subseteq U \to y \subseteq U$
25	24	imim1i	$⊢ (y \subseteq U \to y \in U) \to (y \cup \{z\} \subseteq U \to y \in U)$
26	1	adantr	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to U \in WUni$
27		simprr	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to y \in U$
28		simprl	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to y \cup \{z\} \subseteq U$
29	28	unssbd	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to \{z\} \subseteq U$
30		vex	$⊢ z \in V$
31	30	snss	$⊢ z \in U \leftrightarrow \{z\} \subseteq U$
32	29 31	sylibr	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to z \in U$
33	26 32	wunsn	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to \{z\} \in U$
34	26 27 33	wunun	$⊢ (φ \land (y \cup \{z\} \subseteq U \land y \in U)) \to y \cup \{z\} \in U$
35	34	exp32	$⊢ φ \to (y \cup \{z\} \subseteq U \to (y \in U \to y \cup \{z\} \in U))$
36	35	a2d	$⊢ φ \to ((y \cup \{z\} \subseteq U \to y \in U) \to (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U))$
37	25 36	syl5	$⊢ φ \to ((y \subseteq U \to y \in U) \to (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U))$
38	37	a2i	$⊢ (φ \to (y \subseteq U \to y \in U)) \to (φ \to (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U))$
39	38	a1i	$⊢ y \in Fin \to ((φ \to (y \subseteq U \to y \in U)) \to (φ \to (y \cup \{z\} \subseteq U \to y \cup \{z\} \in U)))$
40	7 11 15 19 21 39	findcard2	$⊢ A \in Fin \to (φ \to (A \subseteq U \to A \in U))$
41	3 40	mpcom	$⊢ φ \to (A \subseteq U \to A \in U)$
42	2 41	mpd	$⊢ φ \to A \in U$

Metamath Proof Explorer

Theorem wunfi

Proof