dnwech

Description: Define a well-ordering from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

	Ref	Expression
Hypotheses	dnnumch.f	$⊢ F = recs ((z \in V ⟼ G (A ∖ ran z)))$
	dnnumch.a	$⊢ φ \to A \in V$
	dnnumch.g	$⊢ φ \to \forall y \in 𝒫 A (y \neq \emptyset \to G (y) \in y)$
	dnwech.h	$⊢ H = \{⟨v, w⟩ \| ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}]\}$
Assertion	dnwech	$⊢ φ \to H We A$

Proof

Step	Hyp	Ref	Expression
1		dnnumch.f	$⊢ F = recs ((z \in V ⟼ G (A ∖ ran z)))$
2		dnnumch.a	$⊢ φ \to A \in V$
3		dnnumch.g	$⊢ φ \to \forall y \in 𝒫 A (y \neq \emptyset \to G (y) \in y)$
4		dnwech.h	$⊢ H = \{⟨v, w⟩ \| ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}]\}$
5	1 2 3	dnnumch3	$⊢ φ \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1}{⟶} On$
6		epweon	$⊢ E We On$
7		eqid	$⊢ \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} = \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\}$
8	7	f1we	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1}{⟶} On \to (E We On \to \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A)$
9	5 6 8	mpisyl	$⊢ φ \to \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A$
10		fvex	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) \in V$
11	10	epeli	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) \leftrightarrow (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) \in (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)$
12	1 2 3	dnnumch3lem	$⊢ (φ \land v \in A) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) = ⋂ F^{-1} [\{v\}]$
13	12	adantrr	$⊢ (φ \land (v \in A \land w \in A)) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) = ⋂ F^{-1} [\{v\}]$
14	1 2 3	dnnumch3lem	$⊢ (φ \land w \in A) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) = ⋂ F^{-1} [\{w\}]$
15	14	adantrl	$⊢ (φ \land (v \in A \land w \in A)) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) = ⋂ F^{-1} [\{w\}]$
16	13 15	eleq12d	$⊢ (φ \land (v \in A \land w \in A)) \to ((x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) \in (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) \leftrightarrow ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}])$
17	11 16	bitr2id	$⊢ (φ \land (v \in A \land w \in A)) \to (⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}] \leftrightarrow (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w))$
18	17	pm5.32da	$⊢ φ \to (((v \in A \land w \in A) \land ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}]) \leftrightarrow ((v \in A \land w \in A) \land (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)))$
19	18	opabbidv	$⊢ φ \to \{⟨v, w⟩ \| ((v \in A \land w \in A) \land ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}])\} = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w))\}$
20		incom	$⊢ H \cap (A \times A) = (A \times A) \cap H$
21		df-xp	$⊢ A \times A = \{⟨v, w⟩ \| (v \in A \land w \in A)\}$
22	21 4	ineq12i	$⊢ (A \times A) \cap H = \{⟨v, w⟩ \| (v \in A \land w \in A)\} \cap \{⟨v, w⟩ \| ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}]\}$
23		inopab	$⊢ \{⟨v, w⟩ \| (v \in A \land w \in A)\} \cap \{⟨v, w⟩ \| ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}]\} = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}])\}$
24	20 22 23	3eqtri	$⊢ H \cap (A \times A) = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}])\}$
25		incom	$⊢ \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A) = (A \times A) \cap \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\}$
26	21	ineq1i	$⊢ (A \times A) \cap \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} = \{⟨v, w⟩ \| (v \in A \land w \in A)\} \cap \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\}$
27		inopab	$⊢ \{⟨v, w⟩ \| (v \in A \land w \in A)\} \cap \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w))\}$
28	25 26 27	3eqtri	$⊢ \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A) = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w))\}$
29	19 24 28	3eqtr4g	$⊢ φ \to H \cap (A \times A) = \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A)$
30		weeq1	$⊢ H \cap (A \times A) = \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A) \to ((H \cap (A \times A)) We A \leftrightarrow (\{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A)) We A)$
31	29 30	syl	$⊢ φ \to ((H \cap (A \times A)) We A \leftrightarrow (\{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A)) We A)$
32		weinxp	$⊢ H We A \leftrightarrow (H \cap (A \times A)) We A$
33		weinxp	$⊢ \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A \leftrightarrow (\{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} \cap (A \times A)) We A$
34	31 32 33	3bitr4g	$⊢ φ \to (H We A \leftrightarrow \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A)$
35	9 34	mpbird	$⊢ φ \to H We A$

Metamath Proof Explorer

Theorem dnwech

Proof