dfatcolem

		Ref	Expression
	Assertion	dfatcolem	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists! y X (F \circ G) y$

Proof

Step	Hyp	Ref	Expression
1		dfdfat2	$⊢ F defAt (G'''' X) \leftrightarrow ((G'''' X) \in dom F \land \exists! y (G'''' X) F y)$
2		eqidd	$⊢ (G defAt X \land F defAt (G'''' X)) \to (G'''' X) = (G'''' X)$
3		df-dfat	$⊢ F defAt (G'''' X) \leftrightarrow ((G'''' X) \in dom F \land Fun ({F ↾}_{\{(G'''' X)\}}))$
4	3	simplbi	$⊢ F defAt (G'''' X) \to (G'''' X) \in dom F$
5		dfatbrafv2b	$⊢ (G defAt X \land (G'''' X) \in dom F) \to ((G'''' X) = (G'''' X) \leftrightarrow X G (G'''' X))$
6	4 5	sylan2	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((G'''' X) = (G'''' X) \leftrightarrow X G (G'''' X))$
7	2 6	mpbid	$⊢ (G defAt X \land F defAt (G'''' X)) \to X G (G'''' X)$
8		eqidd	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F'''' (G'''' X)) = (F'''' (G'''' X))$
9		simpr	$⊢ (G defAt X \land F defAt (G'''' X)) \to F defAt (G'''' X)$
10		dfatafv2ex	$⊢ F defAt (G'''' X) \to (F'''' (G'''' X)) \in V$
11	10	adantl	$⊢ (G defAt X \land F defAt (G'''' X)) \to (F'''' (G'''' X)) \in V$
12		dfatbrafv2b	$⊢ (F defAt (G'''' X) \land (F'''' (G'''' X)) \in V) \to ((F'''' (G'''' X)) = (F'''' (G'''' X)) \leftrightarrow (G'''' X) F (F'''' (G'''' X)))$
13	9 11 12	syl2anc	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((F'''' (G'''' X)) = (F'''' (G'''' X)) \leftrightarrow (G'''' X) F (F'''' (G'''' X)))$
14	8 13	mpbid	$⊢ (G defAt X \land F defAt (G'''' X)) \to (G'''' X) F (F'''' (G'''' X))$
15	4	adantl	$⊢ (G defAt X \land F defAt (G'''' X)) \to (G'''' X) \in dom F$
16		breq2	$⊢ z = (G'''' X) \to (X G z \leftrightarrow X G (G'''' X))$
17	16	adantl	$⊢ (y = (F'''' (G'''' X)) \land z = (G'''' X)) \to (X G z \leftrightarrow X G (G'''' X))$
18		breq12	$⊢ (z = (G'''' X) \land y = (F'''' (G'''' X))) \to (z F y \leftrightarrow (G'''' X) F (F'''' (G'''' X)))$
19	18	ancoms	$⊢ (y = (F'''' (G'''' X)) \land z = (G'''' X)) \to (z F y \leftrightarrow (G'''' X) F (F'''' (G'''' X)))$
20	17 19	anbi12d	$⊢ (y = (F'''' (G'''' X)) \land z = (G'''' X)) \to ((X G z \land z F y) \leftrightarrow (X G (G'''' X) \land (G'''' X) F (F'''' (G'''' X))))$
21	20	spc2egv	$⊢ ((F'''' (G'''' X)) \in V \land (G'''' X) \in dom F) \to ((X G (G'''' X) \land (G'''' X) F (F'''' (G'''' X))) \to \exists y \exists z (X G z \land z F y))$
22	11 15 21	syl2anc	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((X G (G'''' X) \land (G'''' X) F (F'''' (G'''' X))) \to \exists y \exists z (X G z \land z F y))$
23	7 14 22	mp2and	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists y \exists z (X G z \land z F y)$
24		dfdfat2	$⊢ G defAt X \leftrightarrow (X \in dom G \land \exists! z X G z)$
25		tz6.12c-afv2	$⊢ \exists! z X G z \to ((G'''' X) = z \leftrightarrow X G z)$
26	25	adantl	$⊢ (X \in dom G \land \exists! z X G z) \to ((G'''' X) = z \leftrightarrow X G z)$
27	24 26	sylbi	$⊢ G defAt X \to ((G'''' X) = z \leftrightarrow X G z)$
28	27	adantr	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((G'''' X) = z \leftrightarrow X G z)$
29		breq1	$⊢ (G'''' X) = z \to ((G'''' X) F y \leftrightarrow z F y)$
30	29	adantl	$⊢ (F defAt (G'''' X) \land (G'''' X) = z) \to ((G'''' X) F y \leftrightarrow z F y)$
31	30	exbiri	$⊢ F defAt (G'''' X) \to ((G'''' X) = z \to (z F y \to (G'''' X) F y))$
32	31	adantl	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((G'''' X) = z \to (z F y \to (G'''' X) F y))$
33	28 32	sylbird	$⊢ (G defAt X \land F defAt (G'''' X)) \to (X G z \to (z F y \to (G'''' X) F y))$
34	33	impd	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((X G z \land z F y) \to (G'''' X) F y)$
35	34	exlimdv	$⊢ (G defAt X \land F defAt (G'''' X)) \to (\exists z (X G z \land z F y) \to (G'''' X) F y)$
36	35	alrimiv	$⊢ (G defAt X \land F defAt (G'''' X)) \to \forall y (\exists z (X G z \land z F y) \to (G'''' X) F y)$
37		euim	$⊢ (\exists y \exists z (X G z \land z F y) \land \forall y (\exists z (X G z \land z F y) \to (G'''' X) F y)) \to (\exists! y (G'''' X) F y \to \exists! y \exists z (X G z \land z F y))$
38	23 36 37	syl2anc	$⊢ (G defAt X \land F defAt (G'''' X)) \to (\exists! y (G'''' X) F y \to \exists! y \exists z (X G z \land z F y))$
39	38	com12	$⊢ \exists! y (G'''' X) F y \to ((G defAt X \land F defAt (G'''' X)) \to \exists! y \exists z (X G z \land z F y))$
40	39	adantl	$⊢ ((G'''' X) \in dom F \land \exists! y (G'''' X) F y) \to ((G defAt X \land F defAt (G'''' X)) \to \exists! y \exists z (X G z \land z F y))$
41	40	adantl	$⊢ (G defAt X \land ((G'''' X) \in dom F \land \exists! y (G'''' X) F y)) \to ((G defAt X \land F defAt (G'''' X)) \to \exists! y \exists z (X G z \land z F y))$
42	1 41	sylan2b	$⊢ (G defAt X \land F defAt (G'''' X)) \to ((G defAt X \land F defAt (G'''' X)) \to \exists! y \exists z (X G z \land z F y))$
43	42	pm2.43i	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists! y \exists z (X G z \land z F y)$
44		df-dfat	$⊢ G defAt X \leftrightarrow (X \in dom G \land Fun ({G ↾}_{\{X\}}))$
45	44	simplbi	$⊢ G defAt X \to X \in dom G$
46		vex	$⊢ y \in V$
47	46	a1i	$⊢ F defAt (G'''' X) \to y \in V$
48		brcog	$⊢ (X \in dom G \land y \in V) \to (X (F \circ G) y \leftrightarrow \exists z (X G z \land z F y))$
49	45 47 48	syl2an	$⊢ (G defAt X \land F defAt (G'''' X)) \to (X (F \circ G) y \leftrightarrow \exists z (X G z \land z F y))$
50	49	eubidv	$⊢ (G defAt X \land F defAt (G'''' X)) \to (\exists! y X (F \circ G) y \leftrightarrow \exists! y \exists z (X G z \land z F y))$
51	43 50	mpbird	$⊢ (G defAt X \land F defAt (G'''' X)) \to \exists! y X (F \circ G) y$

Metamath Proof Explorer

Theorem dfatcolem

Proof