infxpenc2lem1

	Ref	Expression
Hypotheses	infxpenc2.1	$⊢ φ \to A \in On$
	infxpenc2.2	$⊢ φ \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
	infxpenc2.3	$⊢ W = {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b))$
Assertion	infxpenc2lem1	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to (W \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$

Proof

Step	Hyp	Ref	Expression
1		infxpenc2.1	$⊢ φ \to A \in On$
2		infxpenc2.2	$⊢ φ \to \forall b \in A (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
3		infxpenc2.3	$⊢ W = {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b))$
4	2	r19.21bi	$⊢ (φ \land b \in A) \to (ω \subseteq b \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
5	4	impr	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to \exists w \in (On ∖ 1_{𝑜}) n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w$
6		simpr	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
7		oveq2	$⊢ x = w \to ω ↑_{𝑜} x = ω ↑_{𝑜} w$
8		eqid	$⊢ (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) = (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)$
9		ovex	$⊢ ω ↑_{𝑜} w \in V$
10	7 8 9	fvmpt	$⊢ w \in (On ∖ 1_{𝑜}) \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) (w) = ω ↑_{𝑜} w$
11	10	ad2antrl	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) (w) = ω ↑_{𝑜} w$
12		f1ofo	$⊢ n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w \to n (b) : b \underset{onto}{⟶} ω ↑_{𝑜} w$
13	12	ad2antll	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to n (b) : b \underset{onto}{⟶} ω ↑_{𝑜} w$
14		forn	$⊢ n (b) : b \underset{onto}{⟶} ω ↑_{𝑜} w \to ran n (b) = ω ↑_{𝑜} w$
15	13 14	syl	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to ran n (b) = ω ↑_{𝑜} w$
16	11 15	eqtr4d	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) (w) = ran n (b)$
17		ovex	$⊢ ω ↑_{𝑜} x \in V$
18	17	2a1i	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (x \in (On ∖ 1_{𝑜}) \to ω ↑_{𝑜} x \in V)$
19		omelon	$⊢ ω \in On$
20		1onn	$⊢ 1_{𝑜} \in ω$
21		ondif2	$⊢ ω \in (On ∖ 2_{𝑜}) \leftrightarrow (ω \in On \land 1_{𝑜} \in ω)$
22	19 20 21	mpbir2an	$⊢ ω \in (On ∖ 2_{𝑜})$
23		eldifi	$⊢ x \in (On ∖ 1_{𝑜}) \to x \in On$
24	23	ad2antrl	$⊢ (((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \land (x \in (On ∖ 1_{𝑜}) \land y \in (On ∖ 1_{𝑜}))) \to x \in On$
25		eldifi	$⊢ y \in (On ∖ 1_{𝑜}) \to y \in On$
26	25	ad2antll	$⊢ (((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \land (x \in (On ∖ 1_{𝑜}) \land y \in (On ∖ 1_{𝑜}))) \to y \in On$
27		oecan	$⊢ (ω \in (On ∖ 2_{𝑜}) \land x \in On \land y \in On) \to (ω ↑_{𝑜} x = ω ↑_{𝑜} y \leftrightarrow x = y)$
28	22 24 26 27	mp3an2i	$⊢ (((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \land (x \in (On ∖ 1_{𝑜}) \land y \in (On ∖ 1_{𝑜}))) \to (ω ↑_{𝑜} x = ω ↑_{𝑜} y \leftrightarrow x = y)$
29	28	ex	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to ((x \in (On ∖ 1_{𝑜}) \land y \in (On ∖ 1_{𝑜})) \to (ω ↑_{𝑜} x = ω ↑_{𝑜} y \leftrightarrow x = y))$
30	18 29	dom2lem	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) : On ∖ 1_{𝑜} \underset{1-1}{⟶} V$
31		f1f1orn	$⊢ (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) : On ∖ 1_{𝑜} \underset{1-1}{⟶} V \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) : On ∖ 1_{𝑜} \underset{1-1 onto}{⟶} ran (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)$
32	30 31	syl	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) : On ∖ 1_{𝑜} \underset{1-1 onto}{⟶} ran (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)$
33		simprl	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to w \in (On ∖ 1_{𝑜})$
34		f1ocnvfv	$⊢ ((x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) : On ∖ 1_{𝑜} \underset{1-1 onto}{⟶} ran (x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) \land w \in (On ∖ 1_{𝑜})) \to ((x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) (w) = ran n (b) \to {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b)) = w)$
35	32 33 34	syl2anc	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to ((x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x) (w) = ran n (b) \to {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b)) = w)$
36	16 35	mpd	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to {(x \in (On ∖ 1_{𝑜}) ⟼ ω ↑_{𝑜} x)}^{-1} (ran n (b)) = w$
37	3 36	syl5eq	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to W = w$
38	37	eleq1d	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (W \in (On ∖ 1_{𝑜}) \leftrightarrow w \in (On ∖ 1_{𝑜}))$
39	37	oveq2d	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to ω ↑_{𝑜} W = ω ↑_{𝑜} w$
40	39	f1oeq3d	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W \leftrightarrow n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)$
41	38 40	anbi12d	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to ((W \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W) \leftrightarrow (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w))$
42	6 41	mpbird	$⊢ ((φ \land (b \in A \land ω \subseteq b)) \land (w \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} w)) \to (W \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$
43	5 42	rexlimddv	$⊢ (φ \land (b \in A \land ω \subseteq b)) \to (W \in (On ∖ 1_{𝑜}) \land n (b) : b \underset{1-1 onto}{⟶} ω ↑_{𝑜} W)$

Metamath Proof Explorer

Theorem infxpenc2lem1

Proof