MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1lem1 Structured version   Visualization version   GIF version
Theorem hashf1lem1 14412
Description: Lemma for hashf1 14415. (Contributed by Mario Carneiro, 17-Apr-2015.) (Proof shortened by AV, 14-Aug-2024.)
Hypotheses
Ref Expression
hashf1lem2.1 (πœ‘ β†’ 𝐴 ∈ Fin)
hashf1lem2.2 (πœ‘ β†’ 𝐡 ∈ Fin)
hashf1lem2.3 (πœ‘ β†’ Β¬ 𝑧 ∈ 𝐴)
hashf1lem2.4 (πœ‘ β†’ ((β™―β€˜π΄) + 1) ≀ (β™―β€˜π΅))
hashf1lem1.5 (πœ‘ β†’ 𝐹:𝐴–1-1→𝐡)
Assertion
Ref Expression
hashf1lem1 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β‰ˆ (𝐡 βˆ– ran 𝐹))
Distinct variable groups:   𝑧,𝑓   𝐴,𝑓   𝐡,𝑓   πœ‘,𝑓   𝑓,𝐹
Allowed substitution hints:   πœ‘(𝑧)   𝐴(𝑧)   𝐡(𝑧)   𝐹(𝑧)
Proof of Theorem hashf1lem1
Dummy variables 𝑔 π‘₯ 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hashf1lem2.2 . . . 4 (πœ‘ β†’ 𝐡 ∈ Fin)
2 f1setex 8847 . . . 4 (𝐡 ∈ Fin β†’ {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡} ∈ V)
31, 2syl 17 . . 3 (πœ‘ β†’ {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡} ∈ V)
4 abanssr 4294 . . . 4 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}
54a1i 11 . . 3 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡})
63, 5ssexd 5314 . 2 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ V)
71difexd 5319 . 2 (πœ‘ β†’ (𝐡 βˆ– ran 𝐹) ∈ V)
8 vex 3470 . . . 4 𝑔 ∈ V
9 reseq1 5965 . . . . . 6 (𝑓 = 𝑔 β†’ (𝑓 β†Ύ 𝐴) = (𝑔 β†Ύ 𝐴))
109eqeq1d 2726 . . . . 5 (𝑓 = 𝑔 β†’ ((𝑓 β†Ύ 𝐴) = 𝐹 ↔ (𝑔 β†Ύ 𝐴) = 𝐹))
11 f1eq1 6772 . . . . 5 (𝑓 = 𝑔 β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ↔ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
1210, 11anbi12d 630 . . . 4 (𝑓 = 𝑔 β†’ (((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
138, 12elab 3660 . . 3 (𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
14 f1f 6777 . . . . . . 7 (𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ 𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡)
1514ad2antll 726 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡)
16 ssun2 4165 . . . . . . 7 {𝑧} βŠ† (𝐴 βˆͺ {𝑧})
17 vex 3470 . . . . . . . 8 𝑧 ∈ V
1817snss 4781 . . . . . . 7 (𝑧 ∈ (𝐴 βˆͺ {𝑧}) ↔ {𝑧} βŠ† (𝐴 βˆͺ {𝑧}))
1916, 18mpbir 230 . . . . . 6 𝑧 ∈ (𝐴 βˆͺ {𝑧})
20 ffvelcdm 7073 . . . . . 6 ((𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡 ∧ 𝑧 ∈ (𝐴 βˆͺ {𝑧})) β†’ (π‘”β€˜π‘§) ∈ 𝐡)
2115, 19, 20sylancl 585 . . . . 5 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (π‘”β€˜π‘§) ∈ 𝐡)
22 hashf1lem2.3 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑧 ∈ 𝐴)
2322adantr 480 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ Β¬ 𝑧 ∈ 𝐴)
24 df-ima 5679 . . . . . . . . 9 (𝑔 β€œ 𝐴) = ran (𝑔 β†Ύ 𝐴)
25 simprl 768 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (𝑔 β†Ύ 𝐴) = 𝐹)
2625rneqd 5927 . . . . . . . . 9 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ran (𝑔 β†Ύ 𝐴) = ran 𝐹)
2724, 26eqtrid 2776 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (𝑔 β€œ 𝐴) = ran 𝐹)
2827eleq2d 2811 . . . . . . 7 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ (π‘”β€˜π‘§) ∈ ran 𝐹))
29 simprr 770 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)
3019a1i 11 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑧 ∈ (𝐴 βˆͺ {𝑧}))
31 ssun1 4164 . . . . . . . . 9 𝐴 βŠ† (𝐴 βˆͺ {𝑧})
3231a1i 11 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝐴 βŠ† (𝐴 βˆͺ {𝑧}))
33 f1elima 7254 . . . . . . . 8 ((𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ∧ 𝑧 ∈ (𝐴 βˆͺ {𝑧}) ∧ 𝐴 βŠ† (𝐴 βˆͺ {𝑧})) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ 𝑧 ∈ 𝐴))
3429, 30, 32, 33syl3anc 1368 . . . . . . 7 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ 𝑧 ∈ 𝐴))
3528, 34bitr3d 281 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐴))
3623, 35mtbird 325 . . . . 5 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ Β¬ (π‘”β€˜π‘§) ∈ ran 𝐹)
3721, 36eldifd 3951 . . . 4 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹))
3837ex 412 . . 3 (πœ‘ β†’ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹)))
3913, 38biimtrid 241 . 2 (πœ‘ β†’ (𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹)))
40 hashf1lem1.5 . . . . . . 7 (πœ‘ β†’ 𝐹:𝐴–1-1→𝐡)
41 f1f 6777 . . . . . . 7 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹:𝐴⟢𝐡)
4240, 41syl 17 . . . . . 6 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
4342adantr 480 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹:𝐴⟢𝐡)
44 vex 3470 . . . . . . . 8 π‘₯ ∈ V
4517, 44f1osn 6863 . . . . . . 7 {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯}
46 f1of 6823 . . . . . . 7 ({βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯} β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯})
4745, 46ax-mp 5 . . . . . 6 {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯}
48 eldifi 4118 . . . . . . . 8 (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ π‘₯ ∈ 𝐡)
4948adantl 481 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ π‘₯ ∈ 𝐡)
5049snssd 4804 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {π‘₯} βŠ† 𝐡)
51 fss 6724 . . . . . 6 (({βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯} ∧ {π‘₯} βŠ† 𝐡) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡)
5247, 50, 51sylancr 586 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡)
53 res0 5975 . . . . . . 7 (𝐹 β†Ύ βˆ…) = βˆ…
54 res0 5975 . . . . . . 7 ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…) = βˆ…
5553, 54eqtr4i 2755 . . . . . 6 (𝐹 β†Ύ βˆ…) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…)
56 disjsn 4707 . . . . . . . . 9 ((𝐴 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝐴)
5722, 56sylibr 233 . . . . . . . 8 (πœ‘ β†’ (𝐴 ∩ {𝑧}) = βˆ…)
5857adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐴 ∩ {𝑧}) = βˆ…)
5958reseq2d 5971 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = (𝐹 β†Ύ βˆ…))
6058reseq2d 5971 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…))
6155, 59, 603eqtr4a 2790 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧})))
62 fresaunres1 6754 . . . . 5 ((𝐹:𝐴⟢𝐡 ∧ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡 ∧ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧}))) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹)
6343, 52, 61, 62syl3anc 1368 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹)
64 f1f1orn 6834 . . . . . . . . 9 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6540, 64syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6665adantr 480 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6745a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯})
68 eldifn 4119 . . . . . . . . 9 (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ Β¬ π‘₯ ∈ ran 𝐹)
6968adantl 481 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ Β¬ π‘₯ ∈ ran 𝐹)
70 disjsn 4707 . . . . . . . 8 ((ran 𝐹 ∩ {π‘₯}) = βˆ… ↔ Β¬ π‘₯ ∈ ran 𝐹)
7169, 70sylibr 233 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (ran 𝐹 ∩ {π‘₯}) = βˆ…)
72 f1oun 6842 . . . . . . 7 (((𝐹:𝐴–1-1-ontoβ†’ran 𝐹 ∧ {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯}) ∧ ((𝐴 ∩ {𝑧}) = βˆ… ∧ (ran 𝐹 ∩ {π‘₯}) = βˆ…)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
7366, 67, 58, 71, 72syl22anc 836 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
74 f1of1 6822 . . . . . 6 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}))
7573, 74syl 17 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}))
7643frnd 6715 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ran 𝐹 βŠ† 𝐡)
7776, 50unssd 4178 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (ran 𝐹 βˆͺ {π‘₯}) βŠ† 𝐡)
78 f1ss 6783 . . . . 5 (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}) ∧ (ran 𝐹 βˆͺ {π‘₯}) βŠ† 𝐡) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)
7975, 77, 78syl2anc 583 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)
80 hashf1lem2.1 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ Fin)
8142, 80fexd 7220 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ V)
8281adantr 480 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹 ∈ V)
83 snex 5421 . . . . . 6 {βŸ¨π‘§, π‘₯⟩} ∈ V
84 unexg 7729 . . . . . 6 ((𝐹 ∈ V ∧ {βŸ¨π‘§, π‘₯⟩} ∈ V) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V)
8582, 83, 84sylancl 585 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V)
86 reseq1 5965 . . . . . . . 8 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (𝑓 β†Ύ 𝐴) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴))
8786eqeq1d 2726 . . . . . . 7 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ ((𝑓 β†Ύ 𝐴) = 𝐹 ↔ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹))
88 f1eq1 6772 . . . . . . 7 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ↔ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡))
8987, 88anbi12d 630 . . . . . 6 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9089elabg 3658 . . . . 5 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9185, 90syl 17 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9263, 79, 91mpbir2and 710 . . 3 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})
9392ex 412 . 2 (πœ‘ β†’ (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
9413anbi1i 623 . . 3 ((𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) ↔ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)))
95 simprlr 777 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)
96 f1fn 6778 . . . . . . 7 (𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ 𝑔 Fn (𝐴 βˆͺ {𝑧}))
9795, 96syl 17 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ 𝑔 Fn (𝐴 βˆͺ {𝑧}))
9873adantrl 713 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
99 f1ofn 6824 . . . . . . 7 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧}))
10098, 99syl 17 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧}))
101 eqfnfv 7022 . . . . . 6 ((𝑔 Fn (𝐴 βˆͺ {𝑧}) ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧})) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
10297, 100, 101syl2anc 583 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
103 fvres 6900 . . . . . . . . . . 11 (𝑦 ∈ 𝐴 β†’ ((𝑔 β†Ύ 𝐴)β€˜π‘¦) = (π‘”β€˜π‘¦))
104103eqcomd 2730 . . . . . . . . . 10 (𝑦 ∈ 𝐴 β†’ (π‘”β€˜π‘¦) = ((𝑔 β†Ύ 𝐴)β€˜π‘¦))
105 simprll 776 . . . . . . . . . . 11 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 β†Ύ 𝐴) = 𝐹)
106105fveq1d 6883 . . . . . . . . . 10 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((𝑔 β†Ύ 𝐴)β€˜π‘¦) = (πΉβ€˜π‘¦))
107104, 106sylan9eqr 2786 . . . . . . . . 9 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (π‘”β€˜π‘¦) = (πΉβ€˜π‘¦))
10840ad2antrr 723 . . . . . . . . . . 11 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝐹:𝐴–1-1→𝐡)
109 f1fn 6778 . . . . . . . . . . 11 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹 Fn 𝐴)
110108, 109syl 17 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝐹 Fn 𝐴)
11117, 44fnsn 6596 . . . . . . . . . . 11 {βŸ¨π‘§, π‘₯⟩} Fn {𝑧}
112111a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ {βŸ¨π‘§, π‘₯⟩} Fn {𝑧})
11357ad2antrr 723 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (𝐴 ∩ {𝑧}) = βˆ…)
114 simpr 484 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐴)
115110, 112, 113, 114fvun1d 6974 . . . . . . . . 9 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) = (πΉβ€˜π‘¦))
116107, 115eqtr4d 2767 . . . . . . . 8 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))
117116ralrimiva 3138 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))
118117biantrurd 532 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ∧ βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))))
119 ralunb 4183 . . . . . 6 (βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ∧ βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
120118, 119bitr4di 289 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
12142fdmd 6718 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐹 = 𝐴)
122121eleq2d 2811 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
12322, 122mtbird 325 . . . . . . . . 9 (πœ‘ β†’ Β¬ 𝑧 ∈ dom 𝐹)
124123adantr 480 . . . . . . . 8 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ Β¬ 𝑧 ∈ dom 𝐹)
125 fsnunfv 7177 . . . . . . . 8 ((𝑧 ∈ V ∧ π‘₯ ∈ V ∧ Β¬ 𝑧 ∈ dom 𝐹) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) = π‘₯)
12617, 44, 124, 125mp3an12i 1461 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) = π‘₯)
127126eqeq2d 2735 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) ↔ (π‘”β€˜π‘§) = π‘₯))
128 fveq2 6881 . . . . . . . 8 (𝑦 = 𝑧 β†’ (π‘”β€˜π‘¦) = (π‘”β€˜π‘§))
129 fveq2 6881 . . . . . . . 8 (𝑦 = 𝑧 β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§))
130128, 129eqeq12d 2740 . . . . . . 7 (𝑦 = 𝑧 β†’ ((π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§)))
13117, 130ralsn 4677 . . . . . 6 (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§))
132 eqcom 2731 . . . . . 6 (π‘₯ = (π‘”β€˜π‘§) ↔ (π‘”β€˜π‘§) = π‘₯)
133127, 131, 1323bitr4g 314 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ π‘₯ = (π‘”β€˜π‘§)))
134102, 120, 1333bitr2d 307 . . . 4 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§)))
135134ex 412 . . 3 (πœ‘ β†’ ((((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§))))
13694, 135biimtrid 241 . 2 (πœ‘ β†’ ((𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§))))
1376, 7, 39, 93, 136en3d 8981 1 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β‰ˆ (𝐡 βˆ– ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 395   = wceq 1533   ∈ wcel 2098  {cab 2701  βˆ€wral 3053  Vcvv 3466   βˆ– cdif 3937   βˆͺ cun 3938   ∩ cin 3939   βŠ† wss 3940  βˆ…c0 4314  {csn 4620  βŸ¨cop 4626   class class class wbr 5138  dom cdm 5666  ran crn 5667   β†Ύ cres 5668   β€œ cima 5669   Fn wfn 6528  βŸΆwf 6529  β€“1-1β†’wf1 6530  β€“1-1-ontoβ†’wf1o 6532  β€˜cfv 6533  (class class class)co 7401   β‰ˆ cen 8932  Fincfn 8935  1c1 11107   + caddc 11109   ≀ cle 11246  β™―chash 14287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5275  ax-sep 5289  ax-nul 5296  ax-pow 5353  ax-pr 5417  ax-un 7718
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3770  df-csb 3886  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-pw 4596  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-iun 4989  df-br 5139  df-opab 5201  df-mpt 5222  df-id 5564  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-ov 7404  df-oprab 7405  df-mpo 7406  df-1st 7968  df-2nd 7969  df-map 8818  df-en 8936
This theorem is referenced by:  hashf1lem2  14414
  Copyright terms: Public domain W3C validator