regsfromunir1

		Ref	Expression
	Hypothesis	regsfromunir1.1	$⊢ ⋃ R_{1} [On] = V$
	Assertion	regsfromunir1	$⊢ \exists x φ \to \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$

Proof

Step	Hyp	Ref	Expression
1		regsfromunir1.1	$⊢ ⋃ R_{1} [On] = V$
2		rankf	$⊢ rank : ⋃ R_{1} [On] ⟶ On$
3		fimass	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to rank [\{x \| φ\}] \subseteq On$
4	2 3	ax-mp	$⊢ rank [\{x \| φ\}] \subseteq On$
5		ffn	$⊢ rank : ⋃ R_{1} [On] ⟶ On \to rank Fn ⋃ R_{1} [On]$
6	2 5	ax-mp	$⊢ rank Fn ⋃ R_{1} [On]$
7		ssv	$⊢ \{x \| φ\} \subseteq V$
8	7 1	sseqtrri	$⊢ \{x \| φ\} \subseteq ⋃ R_{1} [On]$
9		fnimaeq0	$⊢ (rank Fn ⋃ R_{1} [On] \land \{x \| φ\} \subseteq ⋃ R_{1} [On]) \to (rank [\{x \| φ\}] = \emptyset \leftrightarrow \{x \| φ\} = \emptyset)$
10	6 8 9	mp2an	$⊢ rank [\{x \| φ\}] = \emptyset \leftrightarrow \{x \| φ\} = \emptyset$
11	10	necon3bii	$⊢ rank [\{x \| φ\}] \neq \emptyset \leftrightarrow \{x \| φ\} \neq \emptyset$
12	11	biimpri	$⊢ \{x \| φ\} \neq \emptyset \to rank [\{x \| φ\}] \neq \emptyset$
13		onint	$⊢ (rank [\{x \| φ\}] \subseteq On \land rank [\{x \| φ\}] \neq \emptyset) \to ⋂ rank [\{x \| φ\}] \in rank [\{x \| φ\}]$
14	4 12 13	sylancr	$⊢ \{x \| φ\} \neq \emptyset \to ⋂ rank [\{x \| φ\}] \in rank [\{x \| φ\}]$
15		abn0	$⊢ \{x \| φ\} \neq \emptyset \leftrightarrow \exists x φ$
16		fvelimab	$⊢ (rank Fn ⋃ R_{1} [On] \land \{x \| φ\} \subseteq ⋃ R_{1} [On]) \to (⋂ rank [\{x \| φ\}] \in rank [\{x \| φ\}] \leftrightarrow \exists y \in \{x \| φ\} rank (y) = ⋂ rank [\{x \| φ\}])$
17	6 8 16	mp2an	$⊢ ⋂ rank [\{x \| φ\}] \in rank [\{x \| φ\}] \leftrightarrow \exists y \in \{x \| φ\} rank (y) = ⋂ rank [\{x \| φ\}]$
18	14 15 17	3imtr3i	$⊢ \exists x φ \to \exists y \in \{x \| φ\} rank (y) = ⋂ rank [\{x \| φ\}]$
19		vex	$⊢ y \in V$
20	19 1	eleqtrri	$⊢ y \in ⋃ R_{1} [On]$
21		rankelb	$⊢ y \in ⋃ R_{1} [On] \to (z \in y \to rank (z) \in rank (y))$
22	20 21	ax-mp	$⊢ z \in y \to rank (z) \in rank (y)$
23		eleq2	$⊢ rank (y) = ⋂ rank [\{x \| φ\}] \to (rank (z) \in rank (y) \leftrightarrow rank (z) \in ⋂ rank [\{x \| φ\}])$
24	23	biimpd	$⊢ rank (y) = ⋂ rank [\{x \| φ\}] \to (rank (z) \in rank (y) \to rank (z) \in ⋂ rank [\{x \| φ\}])$
25		fnfvima	$⊢ (rank Fn ⋃ R_{1} [On] \land \{x \| φ\} \subseteq ⋃ R_{1} [On] \land z \in \{x \| φ\}) \to rank (z) \in rank [\{x \| φ\}]$
26	6 8 25	mp3an12	$⊢ z \in \{x \| φ\} \to rank (z) \in rank [\{x \| φ\}]$
27		onnmin	$⊢ (rank [\{x \| φ\}] \subseteq On \land rank (z) \in rank [\{x \| φ\}]) \to \neg rank (z) \in ⋂ rank [\{x \| φ\}]$
28	4 26 27	sylancr	$⊢ z \in \{x \| φ\} \to \neg rank (z) \in ⋂ rank [\{x \| φ\}]$
29	28	con2i	$⊢ rank (z) \in ⋂ rank [\{x \| φ\}] \to \neg z \in \{x \| φ\}$
30	22 24 29	syl56	$⊢ rank (y) = ⋂ rank [\{x \| φ\}] \to (z \in y \to \neg z \in \{x \| φ\})$
31	30	alrimiv	$⊢ rank (y) = ⋂ rank [\{x \| φ\}] \to \forall z (z \in y \to \neg z \in \{x \| φ\})$
32	31	reximi	$⊢ \exists y \in \{x \| φ\} rank (y) = ⋂ rank [\{x \| φ\}] \to \exists y \in \{x \| φ\} \forall z (z \in y \to \neg z \in \{x \| φ\})$
33		df-rex	$⊢ \exists y \in \{x \| φ\} \forall z (z \in y \to \neg z \in \{x \| φ\}) \leftrightarrow \exists y (y \in \{x \| φ\} \land \forall z (z \in y \to \neg z \in \{x \| φ\}))$
34		df-clab	$⊢ y \in \{x \| φ\} \leftrightarrow [y/ x] φ$
35		sb6	$⊢ [y/ x] φ \leftrightarrow \forall x (x = y \to φ)$
36	34 35	bitri	$⊢ y \in \{x \| φ\} \leftrightarrow \forall x (x = y \to φ)$
37		df-clab	$⊢ z \in \{x \| φ\} \leftrightarrow [z/ x] φ$
38		sb6	$⊢ [z/ x] φ \leftrightarrow \forall x (x = z \to φ)$
39	37 38	bitri	$⊢ z \in \{x \| φ\} \leftrightarrow \forall x (x = z \to φ)$
40	39	notbii	$⊢ \neg z \in \{x \| φ\} \leftrightarrow \neg \forall x (x = z \to φ)$
41	40	imbi2i	$⊢ (z \in y \to \neg z \in \{x \| φ\}) \leftrightarrow (z \in y \to \neg \forall x (x = z \to φ))$
42	41	albii	$⊢ \forall z (z \in y \to \neg z \in \{x \| φ\}) \leftrightarrow \forall z (z \in y \to \neg \forall x (x = z \to φ))$
43	36 42	anbi12i	$⊢ (y \in \{x \| φ\} \land \forall z (z \in y \to \neg z \in \{x \| φ\})) \leftrightarrow (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$
44	43	exbii	$⊢ \exists y (y \in \{x \| φ\} \land \forall z (z \in y \to \neg z \in \{x \| φ\})) \leftrightarrow \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$
45	33 44	sylbb	$⊢ \exists y \in \{x \| φ\} \forall z (z \in y \to \neg z \in \{x \| φ\}) \to \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$
46	18 32 45	3syl	$⊢ \exists x φ \to \exists y (\forall x (x = y \to φ) \land \forall z (z \in y \to \neg \forall x (x = z \to φ)))$

Metamath Proof Explorer

Theorem regsfromunir1

Proof