wwlktovfo

	Ref	Expression
Hypotheses	wwlktovf1o.d	$⊢ D = \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\}$
	wwlktovf1o.r	$⊢ R = \{n \in V \| \{P, n\} \in X\}$
	wwlktovf1o.f	$⊢ F = (t \in D ⟼ t (1))$
Assertion	wwlktovfo	$⊢ P \in V \to F : D \underset{onto}{⟶} R$

Proof

Step	Hyp	Ref	Expression
1		wwlktovf1o.d	$⊢ D = \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\}$
2		wwlktovf1o.r	$⊢ R = \{n \in V \| \{P, n\} \in X\}$
3		wwlktovf1o.f	$⊢ F = (t \in D ⟼ t (1))$
4	1 2 3	wwlktovf	$⊢ F : D ⟶ R$
5	4	a1i	$⊢ P \in V \to F : D ⟶ R$
6		preq2	$⊢ n = p \to \{P, n\} = \{P, p\}$
7	6	eleq1d	$⊢ n = p \to (\{P, n\} \in X \leftrightarrow \{P, p\} \in X)$
8	7 2	elrab2	$⊢ p \in R \leftrightarrow (p \in V \land \{P, p\} \in X)$
9		simpl	$⊢ (p \in V \land \{P, p\} \in X) \to p \in V$
10	9	anim2i	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to (P \in V \land p \in V)$
11		eqidd	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \{⟨0, P⟩, ⟨1, p⟩\} = \{⟨0, P⟩, ⟨1, p⟩\}$
12		wrdlen2i	$⊢ (P \in V \land p \in V) \to (\{⟨0, P⟩, ⟨1, p⟩\} = \{⟨0, P⟩, ⟨1, p⟩\} \to ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)))$
13	10 11 12	sylc	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))$
14		prex	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} \in V$
15	14	a1i	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \{⟨0, P⟩, ⟨1, p⟩\} \in V$
16		eleq1	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \leftrightarrow u \in Word V)$
17	16	biimpd	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \to u \in Word V)$
18	17	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to (\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \to u \in Word V)$
19	18	com12	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} \in Word V \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u \in Word V)$
20	19	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u \in Word V)$
21	20	adantr	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u \in Word V)$
22	21	impcom	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to u \in Word V$
23		fveqeq2	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2 \leftrightarrow \|u\| = 2)$
24	23	biimpd	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2 \to \|u\| = 2)$
25	24	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to (\|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2 \to \|u\| = 2)$
26	25	com12	$⊢ \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2 \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to \|u\| = 2)$
27	26	adantl	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to \|u\| = 2)$
28	27	adantr	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to \|u\| = 2)$
29	28	impcom	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to \|u\| = 2$
30		fveq1	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to \{⟨0, P⟩, ⟨1, p⟩\} (0) = u (0)$
31	30	eqeq1d	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \leftrightarrow u (0) = P)$
32	31	biimpd	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \to u (0) = P)$
33	32	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \to u (0) = P)$
34	33	com12	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} (0) = P \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u (0) = P)$
35	34	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u (0) = P)$
36	35	adantl	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to u (0) = P)$
37	36	impcom	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to u (0) = P$
38		fveq1	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to \{⟨0, P⟩, ⟨1, p⟩\} (1) = u (1)$
39	38	eqeq1d	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} (1) = p \leftrightarrow u (1) = p)$
40	31 39	anbi12d	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to ((\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p) \leftrightarrow (u (0) = P \land u (1) = p))$
41		preq12	$⊢ (u (0) = P \land u (1) = p) \to \{u (0), u (1)\} = \{P, p\}$
42	41	eqcomd	$⊢ (u (0) = P \land u (1) = p) \to \{P, p\} = \{u (0), u (1)\}$
43	42	eleq1d	$⊢ (u (0) = P \land u (1) = p) \to (\{P, p\} \in X \leftrightarrow \{u (0), u (1)\} \in X)$
44	43	biimpd	$⊢ (u (0) = P \land u (1) = p) \to (\{P, p\} \in X \to \{u (0), u (1)\} \in X)$
45	40 44	syl6bi	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to ((\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p) \to (\{P, p\} \in X \to \{u (0), u (1)\} \in X))$
46	45	com12	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p) \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{P, p\} \in X \to \{u (0), u (1)\} \in X))$
47	46	adantl	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{P, p\} \in X \to \{u (0), u (1)\} \in X))$
48	47	com13	$⊢ \{P, p\} \in X \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to \{u (0), u (1)\} \in X))$
49	48	ad2antll	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to \{u (0), u (1)\} \in X))$
50	49	impcom	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to \{u (0), u (1)\} \in X)$
51	50	imp	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to \{u (0), u (1)\} \in X$
52	29 37 51	3jca	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)$
53		eqcom	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} (1) = p \leftrightarrow p = \{⟨0, P⟩, ⟨1, p⟩\} (1)$
54	38	eqeq2d	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (p = \{⟨0, P⟩, ⟨1, p⟩\} (1) \leftrightarrow p = u (1))$
55	54	biimpd	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (p = \{⟨0, P⟩, ⟨1, p⟩\} (1) \to p = u (1))$
56	53 55	syl5bi	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (\{⟨0, P⟩, ⟨1, p⟩\} (1) = p \to p = u (1))$
57	56	com12	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} (1) = p \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to p = u (1))$
58	57	ad2antll	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to (\{⟨0, P⟩, ⟨1, p⟩\} = u \to p = u (1))$
59	58	com12	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to p = u (1))$
60	59	adantr	$⊢ (\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to p = u (1))$
61	60	imp	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to p = u (1)$
62	22 52 61	jca31	$⊢ ((\{⟨0, P⟩, ⟨1, p⟩\} = u \land (P \in V \land (p \in V \land \{P, p\} \in X))) \land ((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p))) \to ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))$
63	62	exp31	$⊢ \{⟨0, P⟩, ⟨1, p⟩\} = u \to ((P \in V \land (p \in V \land \{P, p\} \in X)) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))))$
64	63	eqcoms	$⊢ u = \{⟨0, P⟩, ⟨1, p⟩\} \to ((P \in V \land (p \in V \land \{P, p\} \in X)) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))))$
65	64	impcom	$⊢ ((P \in V \land (p \in V \land \{P, p\} \in X)) \land u = \{⟨0, P⟩, ⟨1, p⟩\}) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1)))$
66	15 65	spcimedv	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to (((\{⟨0, P⟩, ⟨1, p⟩\} \in Word V \land \|\{⟨0, P⟩, ⟨1, p⟩\}\| = 2) \land (\{⟨0, P⟩, ⟨1, p⟩\} (0) = P \land \{⟨0, P⟩, ⟨1, p⟩\} (1) = p)) \to \exists u ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1)))$
67	13 66	mpd	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \exists u ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))$
68		fveqeq2	$⊢ w = u \to (\|w\| = 2 \leftrightarrow \|u\| = 2)$
69		fveq1	$⊢ w = u \to w (0) = u (0)$
70	69	eqeq1d	$⊢ w = u \to (w (0) = P \leftrightarrow u (0) = P)$
71		fveq1	$⊢ w = u \to w (1) = u (1)$
72	69 71	preq12d	$⊢ w = u \to \{w (0), w (1)\} = \{u (0), u (1)\}$
73	72	eleq1d	$⊢ w = u \to (\{w (0), w (1)\} \in X \leftrightarrow \{u (0), u (1)\} \in X)$
74	68 70 73	3anbi123d	$⊢ w = u \to ((\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X) \leftrightarrow (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X))$
75	74	elrab	$⊢ u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} \leftrightarrow (u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X))$
76	75	anbi1i	$⊢ (u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} \land p = u (1)) \leftrightarrow ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))$
77	76	exbii	$⊢ \exists u (u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} \land p = u (1)) \leftrightarrow \exists u ((u \in Word V \land (\|u\| = 2 \land u (0) = P \land \{u (0), u (1)\} \in X)) \land p = u (1))$
78	67 77	sylibr	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \exists u (u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} \land p = u (1))$
79		df-rex	$⊢ \exists u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} p = u (1) \leftrightarrow \exists u (u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} \land p = u (1))$
80	78 79	sylibr	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \exists u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} p = u (1)$
81	1	rexeqi	$⊢ \exists u \in D p = u (1) \leftrightarrow \exists u \in \{w \in Word V \| (\|w\| = 2 \land w (0) = P \land \{w (0), w (1)\} \in X)\} p = u (1)$
82	80 81	sylibr	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \exists u \in D p = u (1)$
83		fveq1	$⊢ t = u \to t (1) = u (1)$
84		fvex	$⊢ u (1) \in V$
85	83 3 84	fvmpt	$⊢ u \in D \to F (u) = u (1)$
86	85	eqeq2d	$⊢ u \in D \to (p = F (u) \leftrightarrow p = u (1))$
87	86	rexbiia	$⊢ \exists u \in D p = F (u) \leftrightarrow \exists u \in D p = u (1)$
88	82 87	sylibr	$⊢ (P \in V \land (p \in V \land \{P, p\} \in X)) \to \exists u \in D p = F (u)$
89	8 88	sylan2b	$⊢ (P \in V \land p \in R) \to \exists u \in D p = F (u)$
90	89	ralrimiva	$⊢ P \in V \to \forall p \in R \exists u \in D p = F (u)$
91		dffo3	$⊢ F : D \underset{onto}{⟶} R \leftrightarrow (F : D ⟶ R \land \forall p \in R \exists u \in D p = F (u))$
92	5 90 91	sylanbrc	$⊢ P \in V \to F : D \underset{onto}{⟶} R$

Metamath Proof Explorer

Theorem wwlktovfo

Proof