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		f1f1orn	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1}{⟶} On \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1 onto}{⟶} ran (x \in A ⟼ ⋂ F^{-1} [\{x\}])$
7	5 6	syl	$⊢ φ \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1 onto}{⟶} ran (x \in A ⟼ ⋂ F^{-1} [\{x\}])$
8		f1f	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1}{⟶} On \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A ⟶ On$
9		frn	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A ⟶ On \to ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]) \subseteq On$
10	5 8 9	3syl	$⊢ φ \to ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]) \subseteq On$
11		epweon	$⊢ E We On$
12		wess	$⊢ ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]) \subseteq On \to (E We On \to E We ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]))$
13	10 11 12	mpisyl	$⊢ φ \to E We ran (x \in A ⟼ ⋂ F^{-1} [\{x\}])$
14		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)\}$
15	14	f1owe	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) : A \underset{1-1 onto}{⟶} ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]) \to (E We ran (x \in A ⟼ ⋂ F^{-1} [\{x\}]) \to \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A)$
16	7 13 15	sylc	$⊢ φ \to \{⟨v, w⟩ \| (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) E (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w)\} We A$
17		fvex	$⊢ (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) \in V$
18	17	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)$
19	1 2 3	dnnumch3lem	$⊢ (φ \land v \in A) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) = ⋂ F^{-1} [\{v\}]$
20	19	adantrr	$⊢ (φ \land (v \in A \land w \in A)) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (v) = ⋂ F^{-1} [\{v\}]$
21	1 2 3	dnnumch3lem	$⊢ (φ \land w \in A) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) = ⋂ F^{-1} [\{w\}]$
22	21	adantrl	$⊢ (φ \land (v \in A \land w \in A)) \to (x \in A ⟼ ⋂ F^{-1} [\{x\}]) (w) = ⋂ F^{-1} [\{w\}]$
23	20 22	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\}])$
24	18 23	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))$
25	24	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)))$
26	25	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))\}$
27		incom	$⊢ H \cap (A \times A) = (A \times A) \cap H$
28		df-xp	$⊢ A \times A = \{⟨v, w⟩ \| (v \in A \land w \in A)\}$
29	28 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\}]\}$
30		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\}])\}$
31	27 29 30	3eqtri	$⊢ H \cap (A \times A) = \{⟨v, w⟩ \| ((v \in A \land w \in A) \land ⋂ F^{-1} [\{v\}] \in ⋂ F^{-1} [\{w\}])\}$
32		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)\}$
33	28	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)\}$
34		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))\}$
35	32 33 34	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))\}$
36	26 31 35	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)$
37		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)$
38	36 37	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)$
39		weinxp	$⊢ H We A \leftrightarrow (H \cap (A \times A)) We A$
40		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$
41	38 39 40	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)$
42	16 41	mpbird	$⊢ φ \to H We A$

Metamath Proof Explorer

Theorem dnwech

Proof