Metamath Proof Explorer


Theorem ttukeylem4

Description: Lemma for ttukey . (Contributed by Mario Carneiro, 15-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 ttukeylem4 φ G = B

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 0elon On
6 1 2 3 4 ttukeylem3 φ On G = if = if = B G G if G F A F
7 5 6 mpan2 φ G = if = if = B G G if G F A F
8 uni0 =
9 8 eqcomi =
10 9 iftruei if = if = B G G if G F A F = if = B G
11 eqid =
12 11 iftruei if = B G = B
13 10 12 eqtri if = if = B G G if G F A F = B
14 7 13 syl6eq φ G = B