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 8848 . . . 4 (𝐡 ∈ Fin β†’ {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡} ∈ V)
31, 2syl 17 . . 3 (πœ‘ β†’ {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡} ∈ V)
4 abanssr 4302 . . . 4 {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡}
54a1i 11 . . 3 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} βŠ† {𝑓 ∣ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡})
63, 5ssexd 5324 . 2 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∈ V)
71difexd 5329 . 2 (πœ‘ β†’ (𝐡 βˆ– ran 𝐹) ∈ V)
8 vex 3479 . . . 4 𝑔 ∈ V
9 reseq1 5974 . . . . . 6 (𝑓 = 𝑔 β†’ (𝑓 β†Ύ 𝐴) = (𝑔 β†Ύ 𝐴))
109eqeq1d 2735 . . . . 5 (𝑓 = 𝑔 β†’ ((𝑓 β†Ύ 𝐴) = 𝐹 ↔ (𝑔 β†Ύ 𝐴) = 𝐹))
11 f1eq1 6780 . . . . 5 (𝑓 = 𝑔 β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ↔ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
1210, 11anbi12d 632 . . . 4 (𝑓 = 𝑔 β†’ (((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
138, 12elab 3668 . . 3 (𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡))
14 f1f 6785 . . . . . . 7 (𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ 𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡)
1514ad2antll 728 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡)
16 ssun2 4173 . . . . . . 7 {𝑧} βŠ† (𝐴 βˆͺ {𝑧})
17 vex 3479 . . . . . . . 8 𝑧 ∈ V
1817snss 4789 . . . . . . 7 (𝑧 ∈ (𝐴 βˆͺ {𝑧}) ↔ {𝑧} βŠ† (𝐴 βˆͺ {𝑧}))
1916, 18mpbir 230 . . . . . 6 𝑧 ∈ (𝐴 βˆͺ {𝑧})
20 ffvelcdm 7081 . . . . . 6 ((𝑔:(𝐴 βˆͺ {𝑧})⟢𝐡 ∧ 𝑧 ∈ (𝐴 βˆͺ {𝑧})) β†’ (π‘”β€˜π‘§) ∈ 𝐡)
2115, 19, 20sylancl 587 . . . . 5 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (π‘”β€˜π‘§) ∈ 𝐡)
22 hashf1lem2.3 . . . . . . 7 (πœ‘ β†’ Β¬ 𝑧 ∈ 𝐴)
2322adantr 482 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ Β¬ 𝑧 ∈ 𝐴)
24 df-ima 5689 . . . . . . . . 9 (𝑔 β€œ 𝐴) = ran (𝑔 β†Ύ 𝐴)
25 simprl 770 . . . . . . . . . 10 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (𝑔 β†Ύ 𝐴) = 𝐹)
2625rneqd 5936 . . . . . . . . 9 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ran (𝑔 β†Ύ 𝐴) = ran 𝐹)
2724, 26eqtrid 2785 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (𝑔 β€œ 𝐴) = ran 𝐹)
2827eleq2d 2820 . . . . . . 7 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ (π‘”β€˜π‘§) ∈ ran 𝐹))
29 simprr 772 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)
3019a1i 11 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝑧 ∈ (𝐴 βˆͺ {𝑧}))
31 ssun1 4172 . . . . . . . . 9 𝐴 βŠ† (𝐴 βˆͺ {𝑧})
3231a1i 11 . . . . . . . 8 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ 𝐴 βŠ† (𝐴 βˆͺ {𝑧}))
33 f1elima 7259 . . . . . . . 8 ((𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ∧ 𝑧 ∈ (𝐴 βˆͺ {𝑧}) ∧ 𝐴 βŠ† (𝐴 βˆͺ {𝑧})) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ 𝑧 ∈ 𝐴))
3429, 30, 32, 33syl3anc 1372 . . . . . . 7 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ (𝑔 β€œ 𝐴) ↔ 𝑧 ∈ 𝐴))
3528, 34bitr3d 281 . . . . . 6 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ ((π‘”β€˜π‘§) ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐴))
3623, 35mtbird 325 . . . . 5 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ Β¬ (π‘”β€˜π‘§) ∈ ran 𝐹)
3721, 36eldifd 3959 . . . 4 ((πœ‘ ∧ ((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)) β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹))
3837ex 414 . . 3 (πœ‘ β†’ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹)))
3913, 38biimtrid 241 . 2 (πœ‘ β†’ (𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β†’ (π‘”β€˜π‘§) ∈ (𝐡 βˆ– ran 𝐹)))
40 hashf1lem1.5 . . . . . . 7 (πœ‘ β†’ 𝐹:𝐴–1-1→𝐡)
41 f1f 6785 . . . . . . 7 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹:𝐴⟢𝐡)
4240, 41syl 17 . . . . . 6 (πœ‘ β†’ 𝐹:𝐴⟢𝐡)
4342adantr 482 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹:𝐴⟢𝐡)
44 vex 3479 . . . . . . . 8 π‘₯ ∈ V
4517, 44f1osn 6871 . . . . . . 7 {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯}
46 f1of 6831 . . . . . . 7 ({βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯} β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯})
4745, 46ax-mp 5 . . . . . 6 {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯}
48 eldifi 4126 . . . . . . . 8 (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ π‘₯ ∈ 𝐡)
4948adantl 483 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ π‘₯ ∈ 𝐡)
5049snssd 4812 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {π‘₯} βŠ† 𝐡)
51 fss 6732 . . . . . 6 (({βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢{π‘₯} ∧ {π‘₯} βŠ† 𝐡) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡)
5247, 50, 51sylancr 588 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡)
53 res0 5984 . . . . . . 7 (𝐹 β†Ύ βˆ…) = βˆ…
54 res0 5984 . . . . . . 7 ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…) = βˆ…
5553, 54eqtr4i 2764 . . . . . 6 (𝐹 β†Ύ βˆ…) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…)
56 disjsn 4715 . . . . . . . . 9 ((𝐴 ∩ {𝑧}) = βˆ… ↔ Β¬ 𝑧 ∈ 𝐴)
5722, 56sylibr 233 . . . . . . . 8 (πœ‘ β†’ (𝐴 ∩ {𝑧}) = βˆ…)
5857adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐴 ∩ {𝑧}) = βˆ…)
5958reseq2d 5980 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = (𝐹 β†Ύ βˆ…))
6058reseq2d 5980 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ βˆ…))
6155, 59, 603eqtr4a 2799 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧})))
62 fresaunres1 6762 . . . . 5 ((𝐹:𝐴⟢𝐡 ∧ {βŸ¨π‘§, π‘₯⟩}:{𝑧}⟢𝐡 ∧ (𝐹 β†Ύ (𝐴 ∩ {𝑧})) = ({βŸ¨π‘§, π‘₯⟩} β†Ύ (𝐴 ∩ {𝑧}))) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹)
6343, 52, 61, 62syl3anc 1372 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹)
64 f1f1orn 6842 . . . . . . . . 9 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6540, 64syl 17 . . . . . . . 8 (πœ‘ β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6665adantr 482 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹:𝐴–1-1-ontoβ†’ran 𝐹)
6745a1i 11 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯})
68 eldifn 4127 . . . . . . . . 9 (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ Β¬ π‘₯ ∈ ran 𝐹)
6968adantl 483 . . . . . . . 8 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ Β¬ π‘₯ ∈ ran 𝐹)
70 disjsn 4715 . . . . . . . 8 ((ran 𝐹 ∩ {π‘₯}) = βˆ… ↔ Β¬ π‘₯ ∈ ran 𝐹)
7169, 70sylibr 233 . . . . . . 7 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (ran 𝐹 ∩ {π‘₯}) = βˆ…)
72 f1oun 6850 . . . . . . 7 (((𝐹:𝐴–1-1-ontoβ†’ran 𝐹 ∧ {βŸ¨π‘§, π‘₯⟩}:{𝑧}–1-1-ontoβ†’{π‘₯}) ∧ ((𝐴 ∩ {𝑧}) = βˆ… ∧ (ran 𝐹 ∩ {π‘₯}) = βˆ…)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
7366, 67, 58, 71, 72syl22anc 838 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
74 f1of1 6830 . . . . . 6 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}))
7573, 74syl 17 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}))
7643frnd 6723 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ran 𝐹 βŠ† 𝐡)
7776, 50unssd 4186 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (ran 𝐹 βˆͺ {π‘₯}) βŠ† 𝐡)
78 f1ss 6791 . . . . 5 (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1β†’(ran 𝐹 βˆͺ {π‘₯}) ∧ (ran 𝐹 βˆͺ {π‘₯}) βŠ† 𝐡) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)
7975, 77, 78syl2anc 585 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)
80 hashf1lem2.1 . . . . . . . 8 (πœ‘ β†’ 𝐴 ∈ Fin)
8142, 80fexd 7226 . . . . . . 7 (πœ‘ β†’ 𝐹 ∈ V)
8281adantr 482 . . . . . 6 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ 𝐹 ∈ V)
83 snex 5431 . . . . . 6 {βŸ¨π‘§, π‘₯⟩} ∈ V
84 unexg 7733 . . . . . 6 ((𝐹 ∈ V ∧ {βŸ¨π‘§, π‘₯⟩} ∈ V) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V)
8582, 83, 84sylancl 587 . . . . 5 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V)
86 reseq1 5974 . . . . . . . 8 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (𝑓 β†Ύ 𝐴) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴))
8786eqeq1d 2735 . . . . . . 7 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ ((𝑓 β†Ύ 𝐴) = 𝐹 ↔ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹))
88 f1eq1 6780 . . . . . . 7 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡 ↔ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡))
8987, 88anbi12d 632 . . . . . 6 (𝑓 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†’ (((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9089elabg 3666 . . . . 5 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ V β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9185, 90syl 17 . . . 4 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ↔ (((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) β†Ύ 𝐴) = 𝐹 ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1→𝐡)))
9263, 79, 91mpbir2and 712 . . 3 ((πœ‘ ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)})
9392ex 414 . 2 (πœ‘ β†’ (π‘₯ ∈ (𝐡 βˆ– ran 𝐹) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)}))
9413anbi1i 625 . . 3 ((𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) ↔ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)))
95 simprlr 779 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡)
96 f1fn 6786 . . . . . . 7 (𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡 β†’ 𝑔 Fn (𝐴 βˆͺ {𝑧}))
9795, 96syl 17 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ 𝑔 Fn (𝐴 βˆͺ {𝑧}))
9873adantrl 715 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}))
99 f1ofn 6832 . . . . . . 7 ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}):(𝐴 βˆͺ {𝑧})–1-1-ontoβ†’(ran 𝐹 βˆͺ {π‘₯}) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧}))
10098, 99syl 17 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧}))
101 eqfnfv 7030 . . . . . 6 ((𝑔 Fn (𝐴 βˆͺ {𝑧}) ∧ (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) Fn (𝐴 βˆͺ {𝑧})) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
10297, 100, 101syl2anc 585 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
103 fvres 6908 . . . . . . . . . . 11 (𝑦 ∈ 𝐴 β†’ ((𝑔 β†Ύ 𝐴)β€˜π‘¦) = (π‘”β€˜π‘¦))
104103eqcomd 2739 . . . . . . . . . 10 (𝑦 ∈ 𝐴 β†’ (π‘”β€˜π‘¦) = ((𝑔 β†Ύ 𝐴)β€˜π‘¦))
105 simprll 778 . . . . . . . . . . 11 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 β†Ύ 𝐴) = 𝐹)
106105fveq1d 6891 . . . . . . . . . 10 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((𝑔 β†Ύ 𝐴)β€˜π‘¦) = (πΉβ€˜π‘¦))
107104, 106sylan9eqr 2795 . . . . . . . . 9 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (π‘”β€˜π‘¦) = (πΉβ€˜π‘¦))
10840ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝐹:𝐴–1-1→𝐡)
109 f1fn 6786 . . . . . . . . . . 11 (𝐹:𝐴–1-1→𝐡 β†’ 𝐹 Fn 𝐴)
110108, 109syl 17 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝐹 Fn 𝐴)
11117, 44fnsn 6604 . . . . . . . . . . 11 {βŸ¨π‘§, π‘₯⟩} Fn {𝑧}
112111a1i 11 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ {βŸ¨π‘§, π‘₯⟩} Fn {𝑧})
11357ad2antrr 725 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (𝐴 ∩ {𝑧}) = βˆ…)
114 simpr 486 . . . . . . . . . 10 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ 𝑦 ∈ 𝐴)
115110, 112, 113, 114fvun1d 6982 . . . . . . . . 9 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) = (πΉβ€˜π‘¦))
116107, 115eqtr4d 2776 . . . . . . . 8 (((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) ∧ 𝑦 ∈ 𝐴) β†’ (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))
117116ralrimiva 3147 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))
118117biantrurd 534 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ∧ βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦))))
119 ralunb 4191 . . . . . 6 (βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (βˆ€π‘¦ ∈ 𝐴 (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ∧ βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
120118, 119bitr4di 289 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ βˆ€π‘¦ ∈ (𝐴 βˆͺ {𝑧})(π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦)))
12142fdmd 6726 . . . . . . . . . . 11 (πœ‘ β†’ dom 𝐹 = 𝐴)
122121eleq2d 2820 . . . . . . . . . 10 (πœ‘ β†’ (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴))
12322, 122mtbird 325 . . . . . . . . 9 (πœ‘ β†’ Β¬ 𝑧 ∈ dom 𝐹)
124123adantr 482 . . . . . . . 8 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ Β¬ 𝑧 ∈ dom 𝐹)
125 fsnunfv 7182 . . . . . . . 8 ((𝑧 ∈ V ∧ π‘₯ ∈ V ∧ Β¬ 𝑧 ∈ dom 𝐹) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) = π‘₯)
12617, 44, 124, 125mp3an12i 1466 . . . . . . 7 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) = π‘₯)
127126eqeq2d 2744 . . . . . 6 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ ((π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§) ↔ (π‘”β€˜π‘§) = π‘₯))
128 fveq2 6889 . . . . . . . 8 (𝑦 = 𝑧 β†’ (π‘”β€˜π‘¦) = (π‘”β€˜π‘§))
129 fveq2 6889 . . . . . . . 8 (𝑦 = 𝑧 β†’ ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§))
130128, 129eqeq12d 2749 . . . . . . 7 (𝑦 = 𝑧 β†’ ((π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§)))
13117, 130ralsn 4685 . . . . . 6 (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ (π‘”β€˜π‘§) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘§))
132 eqcom 2740 . . . . . 6 (π‘₯ = (π‘”β€˜π‘§) ↔ (π‘”β€˜π‘§) = π‘₯)
133127, 131, 1323bitr4g 314 . . . . 5 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (βˆ€π‘¦ ∈ {𝑧} (π‘”β€˜π‘¦) = ((𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩})β€˜π‘¦) ↔ π‘₯ = (π‘”β€˜π‘§)))
134102, 120, 1333bitr2d 307 . . . 4 ((πœ‘ ∧ (((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹))) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§)))
135134ex 414 . . 3 (πœ‘ β†’ ((((𝑔 β†Ύ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 βˆͺ {𝑧})–1-1→𝐡) ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§))))
13694, 135biimtrid 241 . 2 (πœ‘ β†’ ((𝑔 ∈ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} ∧ π‘₯ ∈ (𝐡 βˆ– ran 𝐹)) β†’ (𝑔 = (𝐹 βˆͺ {βŸ¨π‘§, π‘₯⟩}) ↔ π‘₯ = (π‘”β€˜π‘§))))
1376, 7, 39, 93, 136en3d 8982 1 (πœ‘ β†’ {𝑓 ∣ ((𝑓 β†Ύ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 βˆͺ {𝑧})–1-1→𝐡)} β‰ˆ (𝐡 βˆ– ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  βˆ€wral 3062  Vcvv 3475   βˆ– cdif 3945   βˆͺ cun 3946   ∩ cin 3947   βŠ† wss 3948  βˆ…c0 4322  {csn 4628  βŸ¨cop 4634   class class class wbr 5148  dom cdm 5676  ran crn 5677   β†Ύ cres 5678   β€œ cima 5679   Fn wfn 6536  βŸΆwf 6537  β€“1-1β†’wf1 6538  β€“1-1-ontoβ†’wf1o 6540  β€˜cfv 6541  (class class class)co 7406   β‰ˆ cen 8933  Fincfn 8936  1c1 11108   + caddc 11110   ≀ cle 11246  β™―chash 14287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819  df-en 8937
This theorem is referenced by:  hashf1lem2  14414
  Copyright terms: Public domain W3C validator