ssrel

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) Remove dependency on ax-sep , ax-nul , ax-pr . (Revised by KP, 25-Oct-2021) Remove dependency on ax-12 . (Revised by SN, 11-Dec-2024)

		Ref	Expression
	Assertion	ssrel	$⊢ 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		ssel	$⊢ A \subseteq B \to (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B)$
2	1	alrimivv	$⊢ A \subseteq B \to \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B)$
3		df-rel	$⊢ Rel A \leftrightarrow A \subseteq V \times V$
4		df-ss	$⊢ A \subseteq V \times V \leftrightarrow \forall z (z \in A \to z \in (V \times V))$
5	3 4	sylbb	$⊢ Rel A \to \forall z (z \in A \to z \in (V \times V))$
6		elopabw	$⊢ z \in V \to (z \in \{⟨x, y⟩ \| (x \in V \land y \in V)\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V)))$
7	6	elv	$⊢ z \in \{⟨x, y⟩ \| (x \in V \land y \in V)\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V))$
8		simpl	$⊢ (z = ⟨x, y⟩ \land (x \in V \land y \in V)) \to z = ⟨x, y⟩$
9	8	2eximi	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land (x \in V \land y \in V)) \to \exists x \exists y z = ⟨x, y⟩$
10	7 9	sylbi	$⊢ z \in \{⟨x, y⟩ \| (x \in V \land y \in V)\} \to \exists x \exists y z = ⟨x, y⟩$
11		df-xp	$⊢ V \times V = \{⟨x, y⟩ \| (x \in V \land y \in V)\}$
12	10 11	eleq2s	$⊢ z \in (V \times V) \to \exists x \exists y z = ⟨x, y⟩$
13	12	imim2i	$⊢ (z \in A \to z \in (V \times V)) \to (z \in A \to \exists x \exists y z = ⟨x, y⟩)$
14	5 13	sylg	$⊢ Rel A \to \forall z (z \in A \to \exists x \exists y z = ⟨x, y⟩)$
15		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in A \leftrightarrow ⟨x, y⟩ \in A)$
16		eleq1	$⊢ z = ⟨x, y⟩ \to (z \in B \leftrightarrow ⟨x, y⟩ \in B)$
17	15 16	imbi12d	$⊢ z = ⟨x, y⟩ \to ((z \in A \to z \in B) \leftrightarrow (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B))$
18	17	biimprcd	$⊢ (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (z = ⟨x, y⟩ \to (z \in A \to z \in B))$
19	18	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))$
20		19.23vv	$⊢ \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))$
21	19 20	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))$
22	21	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))$
23	22	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))$
24	23	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))$
25	14 24	syl5	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (Rel A \to \forall z (z \in A \to z \in B))$
26		df-ss	$⊢ A \subseteq B \leftrightarrow \forall z (z \in A \to z \in B)$
27	25 26	imbitrrdi	$⊢ \forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to (Rel A \to A \subseteq B)$
28	27	com12	$⊢ Rel A \to (\forall x \forall y (⟨x, y⟩ \in A \to ⟨x, y⟩ \in B) \to A \subseteq B)$
29	2 28	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 ssrel

Proof