undmrnresiss

Description: Two ways of saying the identity relation restricted to the union of the domain and range of a relation is a subset of a relation. Generalization of reflexg . (Contributed by RP, 26-Sep-2020)

		Ref	Expression
	Assertion	undmrnresiss	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq B \leftrightarrow \forall x \forall y (x A y \to (x B x \land y B y))$

Proof

Step	Hyp	Ref	Expression
1		resundi	$⊢ {I ↾}_{(dom A \cup ran A)} = ({I ↾}_{dom A}) \cup ({I ↾}_{ran A})$
2	1	sseq1i	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq B \leftrightarrow ({I ↾}_{dom A}) \cup ({I ↾}_{ran A}) \subseteq B$
3		unss	$⊢ ({I ↾}_{dom A} \subseteq B \land {I ↾}_{ran A} \subseteq B) \leftrightarrow ({I ↾}_{dom A}) \cup ({I ↾}_{ran A}) \subseteq B$
4		relres	$⊢ Rel ({I ↾}_{dom A})$
5		ssrel	$⊢ Rel ({I ↾}_{dom A}) \to ({I ↾}_{dom A} \subseteq B \leftrightarrow \forall x \forall z (⟨x, z⟩ \in ({I ↾}_{dom A}) \to ⟨x, z⟩ \in B))$
6	4 5	ax-mp	$⊢ {I ↾}_{dom A} \subseteq B \leftrightarrow \forall x \forall z (⟨x, z⟩ \in ({I ↾}_{dom A}) \to ⟨x, z⟩ \in B)$
7		vex	$⊢ x \in V$
8	7	eldm	$⊢ x \in dom A \leftrightarrow \exists y x A y$
9		df-br	$⊢ x I z \leftrightarrow ⟨x, z⟩ \in I$
10		vex	$⊢ z \in V$
11	10	ideq	$⊢ x I z \leftrightarrow x = z$
12	9 11	bitr3i	$⊢ ⟨x, z⟩ \in I \leftrightarrow x = z$
13	8 12	anbi12ci	$⊢ (x \in dom A \land ⟨x, z⟩ \in I) \leftrightarrow (x = z \land \exists y x A y)$
14	10	opelresi	$⊢ ⟨x, z⟩ \in ({I ↾}_{dom A}) \leftrightarrow (x \in dom A \land ⟨x, z⟩ \in I)$
15		19.42v	$⊢ \exists y (x = z \land x A y) \leftrightarrow (x = z \land \exists y x A y)$
16	13 14 15	3bitr4i	$⊢ ⟨x, z⟩ \in ({I ↾}_{dom A}) \leftrightarrow \exists y (x = z \land x A y)$
17		df-br	$⊢ x B z \leftrightarrow ⟨x, z⟩ \in B$
18	17	bicomi	$⊢ ⟨x, z⟩ \in B \leftrightarrow x B z$
19	16 18	imbi12i	$⊢ (⟨x, z⟩ \in ({I ↾}_{dom A}) \to ⟨x, z⟩ \in B) \leftrightarrow (\exists y (x = z \land x A y) \to x B z)$
20	19	2albii	$⊢ \forall x \forall z (⟨x, z⟩ \in ({I ↾}_{dom A}) \to ⟨x, z⟩ \in B) \leftrightarrow \forall x \forall z (\exists y (x = z \land x A y) \to x B z)$
21		19.23v	$⊢ \forall y ((x = z \land x A y) \to x B z) \leftrightarrow (\exists y (x = z \land x A y) \to x B z)$
22	21	bicomi	$⊢ (\exists y (x = z \land x A y) \to x B z) \leftrightarrow \forall y ((x = z \land x A y) \to x B z)$
23	22	2albii	$⊢ \forall x \forall z (\exists y (x = z \land x A y) \to x B z) \leftrightarrow \forall x \forall z \forall y ((x = z \land x A y) \to x B z)$
24		alcom	$⊢ \forall z \forall y ((x = z \land x A y) \to x B z) \leftrightarrow \forall y \forall z ((x = z \land x A y) \to x B z)$
25		ancomst	$⊢ ((x = z \land x A y) \to x B z) \leftrightarrow ((x A y \land x = z) \to x B z)$
26		impexp	$⊢ ((x A y \land x = z) \to x B z) \leftrightarrow (x A y \to (x = z \to x B z))$
27	25 26	bitri	$⊢ ((x = z \land x A y) \to x B z) \leftrightarrow (x A y \to (x = z \to x B z))$
28	27	albii	$⊢ \forall z ((x = z \land x A y) \to x B z) \leftrightarrow \forall z (x A y \to (x = z \to x B z))$
29		19.21v	$⊢ \forall z (x A y \to (x = z \to x B z)) \leftrightarrow (x A y \to \forall z (x = z \to x B z))$
30		equcom	$⊢ x = z \leftrightarrow z = x$
31	30	imbi1i	$⊢ (x = z \to x B z) \leftrightarrow (z = x \to x B z)$
32	31	albii	$⊢ \forall z (x = z \to x B z) \leftrightarrow \forall z (z = x \to x B z)$
33		breq2	$⊢ z = x \to (x B z \leftrightarrow x B x)$
34	33	equsalvw	$⊢ \forall z (z = x \to x B z) \leftrightarrow x B x$
35	32 34	bitri	$⊢ \forall z (x = z \to x B z) \leftrightarrow x B x$
36	35	imbi2i	$⊢ (x A y \to \forall z (x = z \to x B z)) \leftrightarrow (x A y \to x B x)$
37	28 29 36	3bitri	$⊢ \forall z ((x = z \land x A y) \to x B z) \leftrightarrow (x A y \to x B x)$
38	37	albii	$⊢ \forall y \forall z ((x = z \land x A y) \to x B z) \leftrightarrow \forall y (x A y \to x B x)$
39	24 38	bitri	$⊢ \forall z \forall y ((x = z \land x A y) \to x B z) \leftrightarrow \forall y (x A y \to x B x)$
40	39	albii	$⊢ \forall x \forall z \forall y ((x = z \land x A y) \to x B z) \leftrightarrow \forall x \forall y (x A y \to x B x)$
41	23 40	bitri	$⊢ \forall x \forall z (\exists y (x = z \land x A y) \to x B z) \leftrightarrow \forall x \forall y (x A y \to x B x)$
42	6 20 41	3bitri	$⊢ {I ↾}_{dom A} \subseteq B \leftrightarrow \forall x \forall y (x A y \to x B x)$
43		relres	$⊢ Rel ({I ↾}_{ran A})$
44		ssrel	$⊢ Rel ({I ↾}_{ran A}) \to ({I ↾}_{ran A} \subseteq B \leftrightarrow \forall y \forall z (⟨y, z⟩ \in ({I ↾}_{ran A}) \to ⟨y, z⟩ \in B))$
45	43 44	ax-mp	$⊢ {I ↾}_{ran A} \subseteq B \leftrightarrow \forall y \forall z (⟨y, z⟩ \in ({I ↾}_{ran A}) \to ⟨y, z⟩ \in B)$
46		vex	$⊢ y \in V$
47	46	elrn	$⊢ y \in ran A \leftrightarrow \exists x x A y$
48		df-br	$⊢ y I z \leftrightarrow ⟨y, z⟩ \in I$
49	10	ideq	$⊢ y I z \leftrightarrow y = z$
50	48 49	bitr3i	$⊢ ⟨y, z⟩ \in I \leftrightarrow y = z$
51	47 50	anbi12ci	$⊢ (y \in ran A \land ⟨y, z⟩ \in I) \leftrightarrow (y = z \land \exists x x A y)$
52	10	opelresi	$⊢ ⟨y, z⟩ \in ({I ↾}_{ran A}) \leftrightarrow (y \in ran A \land ⟨y, z⟩ \in I)$
53		19.42v	$⊢ \exists x (y = z \land x A y) \leftrightarrow (y = z \land \exists x x A y)$
54	51 52 53	3bitr4i	$⊢ ⟨y, z⟩ \in ({I ↾}_{ran A}) \leftrightarrow \exists x (y = z \land x A y)$
55		df-br	$⊢ y B z \leftrightarrow ⟨y, z⟩ \in B$
56	55	bicomi	$⊢ ⟨y, z⟩ \in B \leftrightarrow y B z$
57	54 56	imbi12i	$⊢ (⟨y, z⟩ \in ({I ↾}_{ran A}) \to ⟨y, z⟩ \in B) \leftrightarrow (\exists x (y = z \land x A y) \to y B z)$
58	57	2albii	$⊢ \forall y \forall z (⟨y, z⟩ \in ({I ↾}_{ran A}) \to ⟨y, z⟩ \in B) \leftrightarrow \forall y \forall z (\exists x (y = z \land x A y) \to y B z)$
59		19.23v	$⊢ \forall x ((y = z \land x A y) \to y B z) \leftrightarrow (\exists x (y = z \land x A y) \to y B z)$
60	59	bicomi	$⊢ (\exists x (y = z \land x A y) \to y B z) \leftrightarrow \forall x ((y = z \land x A y) \to y B z)$
61	60	2albii	$⊢ \forall y \forall z (\exists x (y = z \land x A y) \to y B z) \leftrightarrow \forall y \forall z \forall x ((y = z \land x A y) \to y B z)$
62		alrot3	$⊢ \forall x \forall y \forall z ((y = z \land x A y) \to y B z) \leftrightarrow \forall y \forall z \forall x ((y = z \land x A y) \to y B z)$
63		ancomst	$⊢ ((y = z \land x A y) \to y B z) \leftrightarrow ((x A y \land y = z) \to y B z)$
64		impexp	$⊢ ((x A y \land y = z) \to y B z) \leftrightarrow (x A y \to (y = z \to y B z))$
65	63 64	bitri	$⊢ ((y = z \land x A y) \to y B z) \leftrightarrow (x A y \to (y = z \to y B z))$
66	65	albii	$⊢ \forall z ((y = z \land x A y) \to y B z) \leftrightarrow \forall z (x A y \to (y = z \to y B z))$
67		19.21v	$⊢ \forall z (x A y \to (y = z \to y B z)) \leftrightarrow (x A y \to \forall z (y = z \to y B z))$
68		equcom	$⊢ y = z \leftrightarrow z = y$
69	68	imbi1i	$⊢ (y = z \to y B z) \leftrightarrow (z = y \to y B z)$
70	69	albii	$⊢ \forall z (y = z \to y B z) \leftrightarrow \forall z (z = y \to y B z)$
71		breq2	$⊢ z = y \to (y B z \leftrightarrow y B y)$
72	71	equsalvw	$⊢ \forall z (z = y \to y B z) \leftrightarrow y B y$
73	70 72	bitri	$⊢ \forall z (y = z \to y B z) \leftrightarrow y B y$
74	73	imbi2i	$⊢ (x A y \to \forall z (y = z \to y B z)) \leftrightarrow (x A y \to y B y)$
75	66 67 74	3bitri	$⊢ \forall z ((y = z \land x A y) \to y B z) \leftrightarrow (x A y \to y B y)$
76	75	2albii	$⊢ \forall x \forall y \forall z ((y = z \land x A y) \to y B z) \leftrightarrow \forall x \forall y (x A y \to y B y)$
77	61 62 76	3bitr2i	$⊢ \forall y \forall z (\exists x (y = z \land x A y) \to y B z) \leftrightarrow \forall x \forall y (x A y \to y B y)$
78	45 58 77	3bitri	$⊢ {I ↾}_{ran A} \subseteq B \leftrightarrow \forall x \forall y (x A y \to y B y)$
79	42 78	anbi12i	$⊢ ({I ↾}_{dom A} \subseteq B \land {I ↾}_{ran A} \subseteq B) \leftrightarrow (\forall x \forall y (x A y \to x B x) \land \forall x \forall y (x A y \to y B y))$
80		19.26-2	$⊢ \forall x \forall y ((x A y \to x B x) \land (x A y \to y B y)) \leftrightarrow (\forall x \forall y (x A y \to x B x) \land \forall x \forall y (x A y \to y B y))$
81		pm4.76	$⊢ ((x A y \to x B x) \land (x A y \to y B y)) \leftrightarrow (x A y \to (x B x \land y B y))$
82	81	2albii	$⊢ \forall x \forall y ((x A y \to x B x) \land (x A y \to y B y)) \leftrightarrow \forall x \forall y (x A y \to (x B x \land y B y))$
83	79 80 82	3bitr2i	$⊢ ({I ↾}_{dom A} \subseteq B \land {I ↾}_{ran A} \subseteq B) \leftrightarrow \forall x \forall y (x A y \to (x B x \land y B y))$
84	2 3 83	3bitr2i	$⊢ {I ↾}_{(dom A \cup ran A)} \subseteq B \leftrightarrow \forall x \forall y (x A y \to (x B x \land y B y))$

Metamath Proof Explorer

Theorem undmrnresiss

Proof