This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem frinxp

Description: Intersection of well-founded relation with Cartesian product of its field. (Contributed by Mario Carneiro, 10-Jul-2014)

		Ref	Expression
	Assertion	frinxp	$⊢ R Fr A \leftrightarrow (R \cap (A \times A)) Fr A$

Proof

Step	Hyp	Ref	Expression
1		ssel	$⊢ z \subseteq A \to (x \in z \to x \in A)$
2		ssel	$⊢ z \subseteq A \to (y \in z \to y \in A)$
3	1 2	anim12d	$⊢ z \subseteq A \to ((x \in z \land y \in z) \to (x \in A \land y \in A))$
4		brinxp	$⊢ (y \in A \land x \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
5	4	ancoms	$⊢ (x \in A \land y \in A) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
6	3 5	syl6	$⊢ z \subseteq A \to ((x \in z \land y \in z) \to (y R x \leftrightarrow y (R \cap (A \times A)) x))$
7	6	impl	$⊢ ((z \subseteq A \land x \in z) \land y \in z) \to (y R x \leftrightarrow y (R \cap (A \times A)) x)$
8	7	notbid	$⊢ ((z \subseteq A \land x \in z) \land y \in z) \to (\neg y R x \leftrightarrow \neg y (R \cap (A \times A)) x)$
9	8	ralbidva	$⊢ (z \subseteq A \land x \in z) \to (\forall y \in z \neg y R x \leftrightarrow \forall y \in z \neg y (R \cap (A \times A)) x)$
10	9	rexbidva	$⊢ z \subseteq A \to (\exists x \in z \forall y \in z \neg y R x \leftrightarrow \exists x \in z \forall y \in z \neg y (R \cap (A \times A)) x)$
11	10	adantr	$⊢ (z \subseteq A \land z \neq \emptyset) \to (\exists x \in z \forall y \in z \neg y R x \leftrightarrow \exists x \in z \forall y \in z \neg y (R \cap (A \times A)) x)$
12	11	pm5.74i	$⊢ ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y R x) \leftrightarrow ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y (R \cap (A \times A)) x)$
13	12	albii	$⊢ \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y R x) \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y (R \cap (A \times A)) x)$
14		df-fr	$⊢ R Fr A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y R x)$
15		df-fr	$⊢ (R \cap (A \times A)) Fr A \leftrightarrow \forall z ((z \subseteq A \land z \neq \emptyset) \to \exists x \in z \forall y \in z \neg y (R \cap (A \times A)) x)$
16	13 14 15	3bitr4i	$⊢ R Fr A \leftrightarrow (R \cap (A \times A)) Fr A$