Metamath Proof Explorer

Theorem oemapval

Description: Value of the relation T . (Contributed by Mario Carneiro, 28-May-2015)

		Ref	Expression
	Hypotheses	cantnfs.s	$⊢ S = dom (A CNF B)$
		cantnfs.a	$⊢ φ \to A \in On$
		cantnfs.b	$⊢ φ \to B \in On$
		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
		oemapval.f	$⊢ φ \to F \in S$
		oemapval.g	$⊢ φ \to G \in S$
	Assertion	oemapval	$⊢ φ \to (F T G \leftrightarrow \exists z \in B (F (z) \in G (z) \land \forall w \in B (z \in w \to F (w) = G (w))))$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		oemapval.t	$⊢ T = \{⟨x, y⟩ \| \exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w)))\}$
5		oemapval.f	$⊢ φ \to F \in S$
6		oemapval.g	$⊢ φ \to G \in S$
7		fveq1	$⊢ x = F \to x (z) = F (z)$
8		fveq1	$⊢ y = G \to y (z) = G (z)$
9		eleq12	$⊢ (x (z) = F (z) \land y (z) = G (z)) \to (x (z) \in y (z) \leftrightarrow F (z) \in G (z))$
10	7 8 9	syl2an	$⊢ (x = F \land y = G) \to (x (z) \in y (z) \leftrightarrow F (z) \in G (z))$
11		fveq1	$⊢ x = F \to x (w) = F (w)$
12		fveq1	$⊢ y = G \to y (w) = G (w)$
13	11 12	eqeqan12d	$⊢ (x = F \land y = G) \to (x (w) = y (w) \leftrightarrow F (w) = G (w))$
14	13	imbi2d	$⊢ (x = F \land y = G) \to ((z \in w \to x (w) = y (w)) \leftrightarrow (z \in w \to F (w) = G (w)))$
15	14	ralbidv	$⊢ (x = F \land y = G) \to (\forall w \in B (z \in w \to x (w) = y (w)) \leftrightarrow \forall w \in B (z \in w \to F (w) = G (w)))$
16	10 15	anbi12d	$⊢ (x = F \land y = G) \to ((x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w))) \leftrightarrow (F (z) \in G (z) \land \forall w \in B (z \in w \to F (w) = G (w))))$
17	16	rexbidv	$⊢ (x = F \land y = G) \to (\exists z \in B (x (z) \in y (z) \land \forall w \in B (z \in w \to x (w) = y (w))) \leftrightarrow \exists z \in B (F (z) \in G (z) \land \forall w \in B (z \in w \to F (w) = G (w))))$
18	17 4	brabga	$⊢ (F \in S \land G \in S) \to (F T G \leftrightarrow \exists z \in B (F (z) \in G (z) \land \forall w \in B (z \in w \to F (w) = G (w))))$
19	5 6 18	syl2anc	$⊢ φ \to (F T G \leftrightarrow \exists z \in B (F (z) \in G (z) \land \forall w \in B (z \in w \to F (w) = G (w))))$