madeval2

Description: Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

		Ref	Expression
	Assertion	madeval2	$⊢ A \in On \to M (A) = \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$

Proof

Step	Hyp	Ref	Expression
1		madeval	$⊢ A \in On \to M (A) = \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]]$
2		scutcl	$⊢ a ≪_{s} b \to a \|_{s} b \in No$
3		eleq1	$⊢ a \|_{s} b = x \to (a \|_{s} b \in No \leftrightarrow x \in No)$
4	3	biimpd	$⊢ a \|_{s} b = x \to (a \|_{s} b \in No \to x \in No)$
5	2 4	mpan9	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
6	5	rexlimivw	$⊢ \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
7	6	rexlimivw	$⊢ \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
8	7	pm4.71ri	$⊢ \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow (x \in No \land \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x))$
9	8	abbii	$⊢ \{x \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\} = \{x \| (x \in No \land \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x))\}$
10		eleq1	$⊢ y = ⟨a, b⟩ \to (y \in ≪_{s} \leftrightarrow ⟨a, b⟩ \in ≪_{s})$
11		breq1	$⊢ y = ⟨a, b⟩ \to (y \|_{s} x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
12	10 11	anbi12d	$⊢ y = ⟨a, b⟩ \to ((y \in ≪_{s} \land y \|_{s} x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x))$
13	12	rexxp	$⊢ \exists y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) (y \in ≪_{s} \land y \|_{s} x) \leftrightarrow \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
14		imaindm	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s}]$
15		dmscut	$⊢ dom \|_{s} = ≪_{s}$
16	15	ineq2i	$⊢ (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s} = (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}$
17	16	imaeq2i	$⊢ \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s}] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
18	14 17	eqtri	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
19	18	eleq2i	$⊢ x \in \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \leftrightarrow x \in \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
20		vex	$⊢ x \in V$
21	20	elima	$⊢ x \in \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}] \leftrightarrow \exists y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) y \|_{s} x$
22		elin	$⊢ y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) \leftrightarrow (y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land y \in ≪_{s})$
23	22	anbi1i	$⊢ (y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) \land y \|_{s} x) \leftrightarrow ((y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land y \in ≪_{s}) \land y \|_{s} x)$
24		anass	$⊢ ((y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land y \in ≪_{s}) \land y \|_{s} x) \leftrightarrow (y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land (y \in ≪_{s} \land y \|_{s} x))$
25	23 24	bitri	$⊢ (y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) \land y \|_{s} x) \leftrightarrow (y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land (y \in ≪_{s} \land y \|_{s} x))$
26	25	rexbii2	$⊢ \exists y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) y \|_{s} x \leftrightarrow \exists y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) (y \in ≪_{s} \land y \|_{s} x)$
27	19 21 26	3bitri	$⊢ x \in \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \leftrightarrow \exists y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) (y \in ≪_{s} \land y \|_{s} x)$
28		df-br	$⊢ a ≪_{s} b \leftrightarrow ⟨a, b⟩ \in ≪_{s}$
29	28	anbi1i	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land a \|_{s} b = x)$
30		df-ov	$⊢ a \|_{s} b = \|_{s} (⟨a, b⟩)$
31	30	eqeq1i	$⊢ a \|_{s} b = x \leftrightarrow \|_{s} (⟨a, b⟩) = x$
32		scutf	$⊢ \|_{s} : ≪_{s} ⟶ No$
33		ffn	$⊢ \|_{s} : ≪_{s} ⟶ No \to \|_{s} Fn ≪_{s}$
34	32 33	ax-mp	$⊢ \|_{s} Fn ≪_{s}$
35		fnbrfvb	$⊢ (\|_{s} Fn ≪_{s} \land ⟨a, b⟩ \in ≪_{s}) \to (\|_{s} (⟨a, b⟩) = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
36	34 35	mpan	$⊢ ⟨a, b⟩ \in ≪_{s} \to (\|_{s} (⟨a, b⟩) = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
37	31 36	syl5bb	$⊢ ⟨a, b⟩ \in ≪_{s} \to (a \|_{s} b = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
38	37	pm5.32i	$⊢ (⟨a, b⟩ \in ≪_{s} \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
39	29 38	bitri	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
40	39	2rexbii	$⊢ \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
41	13 27 40	3bitr4i	$⊢ x \in \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \leftrightarrow \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)$
42	41	abbi2i	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \{x \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$
43		df-rab	$⊢ \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\} = \{x \| (x \in No \land \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x))\}$
44	9 42 43	3eqtr4i	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$
45	1 44	eqtrdi	$⊢ A \in On \to M (A) = \{x \in No \| \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x)\}$

Metamath Proof Explorer

Theorem madeval2

Proof