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		scutcut	$⊢ a ≪_{s} b \to (a \|_{s} b \in No \land a ≪_{s} \{a \|_{s} b\} \land \{a \|_{s} b\} ≪_{s} b)$
3	2	simp1d	$⊢ a ≪_{s} b \to a \|_{s} b \in No$
4		eleq1	$⊢ a \|_{s} b = x \to (a \|_{s} b \in No \leftrightarrow x \in No)$
5	4	biimpd	$⊢ a \|_{s} b = x \to (a \|_{s} b \in No \to x \in No)$
6	3 5	mpan9	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
7	6	rexlimivw	$⊢ \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
8	7	rexlimivw	$⊢ \exists a \in 𝒫 ⋃ M [A] \exists b \in 𝒫 ⋃ M [A] (a ≪_{s} b \land a \|_{s} b = x) \to x \in No$
9	8	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))$
10	9	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))\}$
11		eleq1	$⊢ y = ⟨a, b⟩ \to (y \in ≪_{s} \leftrightarrow ⟨a, b⟩ \in ≪_{s})$
12		breq1	$⊢ y = ⟨a, b⟩ \to (y \|_{s} x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
13	11 12	anbi12d	$⊢ y = ⟨a, b⟩ \to ((y \in ≪_{s} \land y \|_{s} x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x))$
14	13	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)$
15		imaindm	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s}]$
16		dmscut	$⊢ dom \|_{s} = ≪_{s}$
17	16	ineq2i	$⊢ (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s} = (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}$
18	17	imaeq2i	$⊢ \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap dom \|_{s}] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
19	15 18	eqtri	$⊢ \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] = \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
20	19	eleq2i	$⊢ x \in \|_{s} [𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]] \leftrightarrow x \in \|_{s} [(𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}]$
21		vex	$⊢ x \in V$
22	21	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$
23		elin	$⊢ y \in ((𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \cap ≪_{s}) \leftrightarrow (y \in (𝒫 ⋃ M [A] \times 𝒫 ⋃ M [A]) \land y \in ≪_{s})$
24	23	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)$
25		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))$
26	24 25	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))$
27	26	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)$
28	20 22 27	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)$
29		df-br	$⊢ a ≪_{s} b \leftrightarrow ⟨a, b⟩ \in ≪_{s}$
30	29	anbi1i	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land a \|_{s} b = x)$
31		df-ov	$⊢ a \|_{s} b = \|_{s} (⟨a, b⟩)$
32	31	eqeq1i	$⊢ a \|_{s} b = x \leftrightarrow \|_{s} (⟨a, b⟩) = x$
33		scutf	$⊢ \|_{s} : ≪_{s} ⟶ No$
34		ffn	$⊢ \|_{s} : ≪_{s} ⟶ No \to \|_{s} Fn ≪_{s}$
35	33 34	ax-mp	$⊢ \|_{s} Fn ≪_{s}$
36		fnbrfvb	$⊢ (\|_{s} Fn ≪_{s} \land ⟨a, b⟩ \in ≪_{s}) \to (\|_{s} (⟨a, b⟩) = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
37	35 36	mpan	$⊢ ⟨a, b⟩ \in ≪_{s} \to (\|_{s} (⟨a, b⟩) = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
38	32 37	syl5bb	$⊢ ⟨a, b⟩ \in ≪_{s} \to (a \|_{s} b = x \leftrightarrow ⟨a, b⟩ \|_{s} x)$
39	38	pm5.32i	$⊢ (⟨a, b⟩ \in ≪_{s} \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
40	30 39	bitri	$⊢ (a ≪_{s} b \land a \|_{s} b = x) \leftrightarrow (⟨a, b⟩ \in ≪_{s} \land ⟨a, b⟩ \|_{s} x)$
41	40	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)$
42	14 28 41	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)$
43	42	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)\}$
44		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))\}$
45	10 43 44	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)\}$
46	1 45	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