ssrelf

Description: A subclass relationship depends only on a relation's ordered pairs. Theorem 3.2(i) of Monk1 p. 33. (Contributed by NM, 2-Aug-1994) (Proof shortened by Andrew Salmon, 27-Aug-2011) (Revised by Thierry Arnoux, 6-Nov-2017)

	Ref	Expression
Hypotheses	eqrelrd2.1	$⊢ Ⅎ x φ$
	eqrelrd2.2	$⊢ Ⅎ y φ$
	eqrelrd2.3	$⊢ \underline{Ⅎ} x A$
	eqrelrd2.4	$⊢ \underline{Ⅎ} y A$
	eqrelrd2.5	$⊢ \underline{Ⅎ} x B$
	eqrelrd2.6	$⊢ \underline{Ⅎ} y B$
Assertion	ssrelf	$⊢ Rel A \to (A \subseteq B \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B))$

Proof

Step	Hyp	Ref	Expression
1		eqrelrd2.1	$⊢ Ⅎ x φ$
2		eqrelrd2.2	$⊢ Ⅎ y φ$
3		eqrelrd2.3	$⊢ \underline{Ⅎ} x A$
4		eqrelrd2.4	$⊢ \underline{Ⅎ} y A$
5		eqrelrd2.5	$⊢ \underline{Ⅎ} x B$
6		eqrelrd2.6	$⊢ \underline{Ⅎ} y B$
7	3 5	nfss	$⊢ Ⅎ x A \subseteq B$
8	4 6	nfss	$⊢ Ⅎ y A \subseteq B$
9		ssel	$⊢ A \subseteq B \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B)$
10	8 9	alrimi	$⊢ A \subseteq B \to \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B)$
11	7 10	alrimi	$⊢ A \subseteq B \to \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B)$
12		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in A \leftrightarrow ⟨x, y⟩ \in A)$
13		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in B \leftrightarrow ⟨x, y⟩ \in B)$
14	12 13	imbi12d	$⊢ z = ⟨x, y⟩ \to ((z \in A \to z \in B) \leftrightarrow (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B))$
15	14	biimprcd	$⊢ (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (z = ⟨x, y⟩ \to (z \in A \to z \in B))$
16	15	2alimi	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to \forall x \forall y (z = ⟨x, y⟩ \to (z \in A \to z \in B))$
17	4	nfcri	$⊢ Ⅎ y z \in A$
18	6	nfcri	$⊢ Ⅎ y z \in B$
19	17 18	nfim	$⊢ Ⅎ y (z \in A \to z \in B)$
20	19	19.23	$⊢ \forall y (z = ⟨x, y⟩ \to (z \in A \to z \in B)) \leftrightarrow (\exists y z = ⟨x, y⟩ \to (z \in A \to z \in B))$
21	20	albii	$⊢ \forall x \forall y (z = ⟨x, y⟩ \to (z \in A \to z \in B)) \leftrightarrow \forall x (\exists y z = ⟨x, y⟩ \to (z \in A \to z \in B))$
22	3	nfcri	$⊢ Ⅎ x z \in A$
23	5	nfcri	$⊢ Ⅎ x z \in B$
24	22 23	nfim	$⊢ Ⅎ x (z \in A \to z \in B)$
25	24	19.23	$⊢ \forall x (\exists y z = ⟨x, y⟩ \to (z \in A \to z \in B)) \leftrightarrow (\exists x \exists y z = ⟨x, y⟩ \to (z \in A \to z \in B))$
26	21 25	bitri	$⊢ \forall x \forall y (z = ⟨x, y⟩ \to (z \in A \to z \in B)) \leftrightarrow (\exists x \exists y z = ⟨x, y⟩ \to (z \in A \to z \in B))$
27	16 26	sylib	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (\exists x \exists y z = ⟨x, y⟩ \to (z \in A \to z \in B))$
28	27	com23	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (z \in A \to (\exists x \exists y z = ⟨x, y⟩ \to z \in B))$
29	28	a2d	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to ((z \in A \to \exists x \exists y z = ⟨x, y⟩) \to (z \in A \to z \in B))$
30	29	alimdv	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (\forall z (z \in A \to \exists x \exists y z = ⟨x, y⟩) \to \forall z (z \in A \to z \in B))$
31		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
32		dfss2	$⊢ A \subseteq V \times V \leftrightarrow \forall z (z \in A \to z \in (V \times V))$
33		elvv	$⊢ z \in (V \times V) \leftrightarrow \exists x \exists y z = ⟨x, y⟩$
34	33	imbi2i	$⊢ (z \in A \to z \in (V \times V)) \leftrightarrow (z \in A \to \exists x \exists y z = ⟨x, y⟩)$
35	34	albii	$⊢ \forall z (z \in A \to z \in (V \times V)) \leftrightarrow \forall z (z \in A \to \exists x \exists y z = ⟨x, y⟩)$
36	31 32 35	3bitri	$⊢ Rel A \leftrightarrow \forall z (z \in A \to \exists x \exists y z = ⟨x, y⟩)$
37		dfss2	$⊢ A \subseteq B \leftrightarrow \forall z (z \in A \to z \in B)$
38	30 36 37	3imtr4g	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (Rel A \to A \subseteq B)$
39	38	com12	$⊢ Rel A \to (\forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to A \subseteq B)$
40	11 39	impbid2	$⊢ Rel A \to (A \subseteq B \leftrightarrow \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B))$

Metamath Proof Explorer

Theorem ssrelf

Proof