dfhe3

Description: The property of relation R being hereditary in class A . (Contributed by RP, 27-Mar-2020)

		Ref	Expression
	Assertion	dfhe3	$⊢ R hereditary A \leftrightarrow \forall x (x \in A \to \forall y (x R y \to y \in A))$

Proof

Step	Hyp	Ref	Expression
1		df-he	$⊢ R hereditary A \leftrightarrow R [A] \subseteq A$
2		19.21v	$⊢ \forall y (x \in A \to (x R y \to y \in A)) \leftrightarrow (x \in A \to \forall y (x R y \to y \in A))$
3	2	bicomi	$⊢ (x \in A \to \forall y (x R y \to y \in A)) \leftrightarrow \forall y (x \in A \to (x R y \to y \in A))$
4	3	albii	$⊢ \forall x (x \in A \to \forall y (x R y \to y \in A)) \leftrightarrow \forall x \forall y (x \in A \to (x R y \to y \in A))$
5		alcom	$⊢ \forall x \forall y (x \in A \to (x R y \to y \in A)) \leftrightarrow \forall y \forall x (x \in A \to (x R y \to y \in A))$
6		impexp	$⊢ ((x \in A \land x R y) \to y \in A) \leftrightarrow (x \in A \to (x R y \to y \in A))$
7	6	bicomi	$⊢ (x \in A \to (x R y \to y \in A)) \leftrightarrow ((x \in A \land x R y) \to y \in A)$
8	7	albii	$⊢ \forall x (x \in A \to (x R y \to y \in A)) \leftrightarrow \forall x ((x \in A \land x R y) \to y \in A)$
9		19.23v	$⊢ \forall x ((x \in A \land x R y) \to y \in A) \leftrightarrow (\exists x (x \in A \land x R y) \to y \in A)$
10	8 9	bitri	$⊢ \forall x (x \in A \to (x R y \to y \in A)) \leftrightarrow (\exists x (x \in A \land x R y) \to y \in A)$
11	10	albii	$⊢ \forall y \forall x (x \in A \to (x R y \to y \in A)) \leftrightarrow \forall y (\exists x (x \in A \land x R y) \to y \in A)$
12	4 5 11	3bitri	$⊢ \forall x (x \in A \to \forall y (x R y \to y \in A)) \leftrightarrow \forall y (\exists x (x \in A \land x R y) \to y \in A)$
13		df-ss	$⊢ \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \subseteq A \leftrightarrow \forall y (y \in \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \to y \in A)$
14		vex	$⊢ y \in V$
15		opeq2	$⊢ z = y \to ⟨x, z⟩ = ⟨x, y⟩$
16	15	eleq1d	$⊢ z = y \to (⟨x, z⟩ \in R \leftrightarrow ⟨x, y⟩ \in R)$
17		df-br	$⊢ x R y \leftrightarrow ⟨x, y⟩ \in R$
18	16 17	bitr4di	$⊢ z = y \to (⟨x, z⟩ \in R \leftrightarrow x R y)$
19	18	anbi2d	$⊢ z = y \to ((x \in A \land ⟨x, z⟩ \in R) \leftrightarrow (x \in A \land x R y))$
20	19	exbidv	$⊢ z = y \to (\exists x (x \in A \land ⟨x, z⟩ \in R) \leftrightarrow \exists x (x \in A \land x R y))$
21	14 20	elab	$⊢ y \in \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \leftrightarrow \exists x (x \in A \land x R y)$
22	21	imbi1i	$⊢ (y \in \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \to y \in A) \leftrightarrow (\exists x (x \in A \land x R y) \to y \in A)$
23	22	albii	$⊢ \forall y (y \in \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \to y \in A) \leftrightarrow \forall y (\exists x (x \in A \land x R y) \to y \in A)$
24	13 23	bitr2i	$⊢ \forall y (\exists x (x \in A \land x R y) \to y \in A) \leftrightarrow \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \subseteq A$
25		dfima3	$⊢ R [A] = \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\}$
26	25	eqcomi	$⊢ \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} = R [A]$
27	26	sseq1i	$⊢ \{z \| \exists x (x \in A \land ⟨x, z⟩ \in R)\} \subseteq A \leftrightarrow R [A] \subseteq A$
28	24 27	bitri	$⊢ \forall y (\exists x (x \in A \land x R y) \to y \in A) \leftrightarrow R [A] \subseteq A$
29	12 28	bitr2i	$⊢ R [A] \subseteq A \leftrightarrow \forall x (x \in A \to \forall y (x R y \to y \in A))$
30	1 29	bitri	$⊢ R hereditary A \leftrightarrow \forall x (x \in A \to \forall y (x R y \to y \in A))$

Metamath Proof Explorer

Theorem dfhe3

Proof