Metamath Proof Explorer


Theorem ttukeylem3

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 11-May-2015)

Ref Expression
Hypotheses ttukeylem.1 φ F : card A B 1-1 onto A B
ttukeylem.2 φ B A
ttukeylem.3 φ x x A 𝒫 x Fin A
ttukeylem.4 G = recs z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z
Assertion ttukeylem3 φ C On G C = if C = C if C = B G C G C if G C F C A F C

Proof

Step Hyp Ref Expression
1 ttukeylem.1 φ F : card A B 1-1 onto A B
2 ttukeylem.2 φ B A
3 ttukeylem.3 φ x x A 𝒫 x Fin A
4 ttukeylem.4 G = recs z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z
5 4 tfr2 C On G C = z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z G C
6 5 adantl φ C On G C = z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z G C
7 eqidd φ C On z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z = z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z
8 simpr φ C On z = G C z = G C
9 8 dmeqd φ C On z = G C dom z = dom G C
10 4 tfr1 G Fn On
11 onss C On C On
12 11 ad2antlr φ C On z = G C C On
13 fnssres G Fn On C On G C Fn C
14 10 12 13 sylancr φ C On z = G C G C Fn C
15 fndm G C Fn C dom G C = C
16 14 15 syl φ C On z = G C dom G C = C
17 9 16 eqtrd φ C On z = G C dom z = C
18 17 unieqd φ C On z = G C dom z = C
19 17 18 eqeq12d φ C On z = G C dom z = dom z C = C
20 17 eqeq1d φ C On z = G C dom z = C =
21 8 rneqd φ C On z = G C ran z = ran G C
22 df-ima G C = ran G C
23 21 22 syl6eqr φ C On z = G C ran z = G C
24 23 unieqd φ C On z = G C ran z = G C
25 20 24 ifbieq2d φ C On z = G C if dom z = B ran z = if C = B G C
26 8 18 fveq12d φ C On z = G C z dom z = G C C
27 18 fveq2d φ C On z = G C F dom z = F C
28 27 sneqd φ C On z = G C F dom z = F C
29 26 28 uneq12d φ C On z = G C z dom z F dom z = G C C F C
30 29 eleq1d φ C On z = G C z dom z F dom z A G C C F C A
31 eqidd φ C On z = G C =
32 30 28 31 ifbieq12d φ C On z = G C if z dom z F dom z A F dom z = if G C C F C A F C
33 26 32 uneq12d φ C On z = G C z dom z if z dom z F dom z A F dom z = G C C if G C C F C A F C
34 19 25 33 ifbieq12d φ C On z = G C if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z = if C = C if C = B G C G C C if G C C F C A F C
35 onuni C On C On
36 35 ad3antlr φ C On z = G C ¬ C = C C On
37 sucidg C On C suc C
38 36 37 syl φ C On z = G C ¬ C = C C suc C
39 eloni C On Ord C
40 39 ad2antlr φ C On z = G C Ord C
41 orduniorsuc Ord C C = C C = suc C
42 40 41 syl φ C On z = G C C = C C = suc C
43 42 orcanai φ C On z = G C ¬ C = C C = suc C
44 38 43 eleqtrrd φ C On z = G C ¬ C = C C C
45 44 fvresd φ C On z = G C ¬ C = C G C C = G C
46 45 uneq1d φ C On z = G C ¬ C = C G C C F C = G C F C
47 46 eleq1d φ C On z = G C ¬ C = C G C C F C A G C F C A
48 47 ifbid φ C On z = G C ¬ C = C if G C C F C A F C = if G C F C A F C
49 45 48 uneq12d φ C On z = G C ¬ C = C G C C if G C C F C A F C = G C if G C F C A F C
50 49 ifeq2da φ C On z = G C if C = C if C = B G C G C C if G C C F C A F C = if C = C if C = B G C G C if G C F C A F C
51 34 50 eqtrd φ C On z = G C if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z = if C = C if C = B G C G C if G C F C A F C
52 fnfun G Fn On Fun G
53 10 52 ax-mp Fun G
54 simpr φ C On C On
55 resfunexg Fun G C On G C V
56 53 54 55 sylancr φ C On G C V
57 2 elexd φ B V
58 funimaexg Fun G C On G C V
59 53 58 mpan C On G C V
60 59 uniexd C On G C V
61 ifcl B V G C V if C = B G C V
62 57 60 61 syl2an φ C On if C = B G C V
63 fvex G C V
64 snex F C V
65 0ex V
66 64 65 ifex if G C F C A F C V
67 63 66 unex G C if G C F C A F C V
68 ifcl if C = B G C V G C if G C F C A F C V if C = C if C = B G C G C if G C F C A F C V
69 62 67 68 sylancl φ C On if C = C if C = B G C G C if G C F C A F C V
70 7 51 56 69 fvmptd φ C On z V if dom z = dom z if dom z = B ran z z dom z if z dom z F dom z A F dom z G C = if C = C if C = B G C G C if G C F C A F C
71 6 70 eqtrd φ C On G C = if C = C if C = B G C G C if G C F C A F C