rgrusgrprc

Description: The class of 0-regular simple graphs is a proper class. (Contributed by AV, 27-Dec-2020)

		Ref	Expression
	Assertion	rgrusgrprc	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} \notin V$

Proof

Step	Hyp	Ref	Expression
1		elopab	$⊢ p \in \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \leftrightarrow \exists v \exists e (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset)$
2		f0bi	$⊢ e : \emptyset ⟶ \emptyset \leftrightarrow e = \emptyset$
3		opeq2	$⊢ e = \emptyset \to ⟨v, e⟩ = ⟨v, \emptyset⟩$
4		usgr0eop	$⊢ v \in V \to ⟨v, \emptyset⟩ \in USGraph$
5	4	elv	$⊢ ⟨v, \emptyset⟩ \in USGraph$
6	3 5	eqeltrdi	$⊢ e = \emptyset \to ⟨v, e⟩ \in USGraph$
7		vex	$⊢ v \in V$
8		vex	$⊢ e \in V$
9	7 8	opiedgfvi	$⊢ iEdg (⟨v, e⟩) = e$
10		id	$⊢ e = \emptyset \to e = \emptyset$
11	9 10	eqtrid	$⊢ e = \emptyset \to iEdg (⟨v, e⟩) = \emptyset$
12	6 11	jca	$⊢ e = \emptyset \to (⟨v, e⟩ \in USGraph \land iEdg (⟨v, e⟩) = \emptyset)$
13	2 12	sylbi	$⊢ e : \emptyset ⟶ \emptyset \to (⟨v, e⟩ \in USGraph \land iEdg (⟨v, e⟩) = \emptyset)$
14	13	adantl	$⊢ (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to (⟨v, e⟩ \in USGraph \land iEdg (⟨v, e⟩) = \emptyset)$
15		eleq1	$⊢ p = ⟨v, e⟩ \to (p \in USGraph \leftrightarrow ⟨v, e⟩ \in USGraph)$
16		fveqeq2	$⊢ p = ⟨v, e⟩ \to (iEdg (p) = \emptyset \leftrightarrow iEdg (⟨v, e⟩) = \emptyset)$
17	15 16	anbi12d	$⊢ p = ⟨v, e⟩ \to ((p \in USGraph \land iEdg (p) = \emptyset) \leftrightarrow (⟨v, e⟩ \in USGraph \land iEdg (⟨v, e⟩) = \emptyset))$
18	17	adantr	$⊢ (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to ((p \in USGraph \land iEdg (p) = \emptyset) \leftrightarrow (⟨v, e⟩ \in USGraph \land iEdg (⟨v, e⟩) = \emptyset))$
19	14 18	mpbird	$⊢ (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to (p \in USGraph \land iEdg (p) = \emptyset)$
20		fveqeq2	$⊢ g = p \to (iEdg (g) = \emptyset \leftrightarrow iEdg (p) = \emptyset)$
21	20	elrab	$⊢ p \in \{g \in USGraph \| iEdg (g) = \emptyset\} \leftrightarrow (p \in USGraph \land iEdg (p) = \emptyset)$
22	19 21	sylibr	$⊢ (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to p \in \{g \in USGraph \| iEdg (g) = \emptyset\}$
23	22	exlimivv	$⊢ \exists v \exists e (p = ⟨v, e⟩ \land e : \emptyset ⟶ \emptyset) \to p \in \{g \in USGraph \| iEdg (g) = \emptyset\}$
24	1 23	sylbi	$⊢ p \in \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \to p \in \{g \in USGraph \| iEdg (g) = \emptyset\}$
25	24	ssriv	$⊢ \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \subseteq \{g \in USGraph \| iEdg (g) = \emptyset\}$
26		eqid	$⊢ \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} = \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\}$
27	26	griedg0prc	$⊢ \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \notin V$
28		prcssprc	$⊢ (\{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \subseteq \{g \in USGraph \| iEdg (g) = \emptyset\} \land \{⟨v, e⟩ \| e : \emptyset ⟶ \emptyset\} \notin V) \to \{g \in USGraph \| iEdg (g) = \emptyset\} \notin V$
29	25 27 28	mp2an	$⊢ \{g \in USGraph \| iEdg (g) = \emptyset\} \notin V$
30		df-3an	$⊢ (g \in USGraph \land 0 \in ℕ_{0}^{} \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0) \leftrightarrow ((g \in USGraph \land 0 \in ℕ_{0}^{}) \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0)$
31	30	bicomi	$⊢ ((g \in USGraph \land 0 \in ℕ_{0}^{}) \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0) \leftrightarrow (g \in USGraph \land 0 \in ℕ_{0}^{} \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0)$
32	31	a1i	$⊢ g \in USGraph \to (((g \in USGraph \land 0 \in ℕ_{0}^{}) \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0) \leftrightarrow (g \in USGraph \land 0 \in ℕ_{0}^{} \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0))$
33		0xnn0	$⊢ 0 \in ℕ_{0}^{*}$
34		ibar	$⊢ (g \in USGraph \land 0 \in ℕ_{0}^{}) \to (\forall v \in Vtx (g) VtxDeg (g) (v) = 0 \leftrightarrow ((g \in USGraph \land 0 \in ℕ_{0}^{}) \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0))$
35	33 34	mpan2	$⊢ g \in USGraph \to (\forall v \in Vtx (g) VtxDeg (g) (v) = 0 \leftrightarrow ((g \in USGraph \land 0 \in ℕ_{0}^{*}) \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0))$
36		eqid	$⊢ Vtx (g) = Vtx (g)$
37		eqid	$⊢ VtxDeg (g) = VtxDeg (g)$
38	36 37	isrusgr0	$⊢ (g \in USGraph \land 0 \in ℕ_{0}^{}) \to (g RegUSGraph 0 \leftrightarrow (g \in USGraph \land 0 \in ℕ_{0}^{} \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0))$
39	33 38	mpan2	$⊢ g \in USGraph \to (g RegUSGraph 0 \leftrightarrow (g \in USGraph \land 0 \in ℕ_{0}^{*} \land \forall v \in Vtx (g) VtxDeg (g) (v) = 0))$
40	32 35 39	3bitr4d	$⊢ g \in USGraph \to (\forall v \in Vtx (g) VtxDeg (g) (v) = 0 \leftrightarrow g RegUSGraph 0)$
41	40	rabbiia	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} = \{g \in USGraph \| g RegUSGraph 0\}$
42		usgr0edg0rusgr	$⊢ g \in USGraph \to (g RegUSGraph 0 \leftrightarrow Edg (g) = \emptyset)$
43		usgruhgr	$⊢ g \in USGraph \to g \in UHGraph$
44		uhgriedg0edg0	$⊢ g \in UHGraph \to (Edg (g) = \emptyset \leftrightarrow iEdg (g) = \emptyset)$
45	43 44	syl	$⊢ g \in USGraph \to (Edg (g) = \emptyset \leftrightarrow iEdg (g) = \emptyset)$
46	42 45	bitrd	$⊢ g \in USGraph \to (g RegUSGraph 0 \leftrightarrow iEdg (g) = \emptyset)$
47	46	rabbiia	$⊢ \{g \in USGraph \| g RegUSGraph 0\} = \{g \in USGraph \| iEdg (g) = \emptyset\}$
48	41 47	eqtri	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} = \{g \in USGraph \| iEdg (g) = \emptyset\}$
49		neleq1	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} = \{g \in USGraph \| iEdg (g) = \emptyset\} \to (\{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} \notin V \leftrightarrow \{g \in USGraph \| iEdg (g) = \emptyset\} \notin V)$
50	48 49	ax-mp	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} \notin V \leftrightarrow \{g \in USGraph \| iEdg (g) = \emptyset\} \notin V$
51	29 50	mpbir	$⊢ \{g \in USGraph \| \forall v \in Vtx (g) VtxDeg (g) (v) = 0\} \notin V$

Metamath Proof Explorer

Theorem rgrusgrprc

Proof