MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1lem1 Structured version   Visualization version   GIF version

Theorem hashf1lem1 13177
Description: Lemma for hashf1 13179. (Contributed by Mario Carneiro, 17-Apr-2015.)
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 f1f 6058 . . . . . 6 (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
21adantl 482 . . . . 5 (((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)
3 hashf1lem2.2 . . . . . 6 (𝜑𝐵 ∈ Fin)
4 hashf1lem2.1 . . . . . . 7 (𝜑𝐴 ∈ Fin)
5 snfi 7982 . . . . . . 7 {𝑧} ∈ Fin
6 unfi 8171 . . . . . . 7 ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin)
74, 5, 6sylancl 693 . . . . . 6 (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin)
83, 7elmapd 7816 . . . . 5 (𝜑 → (𝑓 ∈ (𝐵𝑚 (𝐴 ∪ {𝑧})) ↔ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵))
92, 8syl5ibr 236 . . . 4 (𝜑 → (((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) → 𝑓 ∈ (𝐵𝑚 (𝐴 ∪ {𝑧}))))
109abssdv 3655 . . 3 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ (𝐵𝑚 (𝐴 ∪ {𝑧})))
11 ovex 6632 . . 3 (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ V
12 ssexg 4764 . . 3 (({𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ⊆ (𝐵𝑚 (𝐴 ∪ {𝑧})) ∧ (𝐵𝑚 (𝐴 ∪ {𝑧})) ∈ V) → {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ V)
1310, 11, 12sylancl 693 . 2 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∈ V)
14 difexg 4768 . . 3 (𝐵 ∈ Fin → (𝐵 ∖ ran 𝐹) ∈ V)
153, 14syl 17 . 2 (𝜑 → (𝐵 ∖ ran 𝐹) ∈ V)
16 vex 3189 . . . 4 𝑔 ∈ V
17 reseq1 5350 . . . . . 6 (𝑓 = 𝑔 → (𝑓𝐴) = (𝑔𝐴))
1817eqeq1d 2623 . . . . 5 (𝑓 = 𝑔 → ((𝑓𝐴) = 𝐹 ↔ (𝑔𝐴) = 𝐹))
19 f1eq1 6053 . . . . 5 (𝑓 = 𝑔 → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵𝑔:(𝐴 ∪ {𝑧})–1-1𝐵))
2018, 19anbi12d 746 . . . 4 (𝑓 = 𝑔 → (((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)))
2116, 20elab 3333 . . 3 (𝑔 ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ↔ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵))
22 f1f 6058 . . . . . . 7 (𝑔:(𝐴 ∪ {𝑧})–1-1𝐵𝑔:(𝐴 ∪ {𝑧})⟶𝐵)
2322ad2antll 764 . . . . . 6 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑔:(𝐴 ∪ {𝑧})⟶𝐵)
24 ssun2 3755 . . . . . . 7 {𝑧} ⊆ (𝐴 ∪ {𝑧})
25 vex 3189 . . . . . . . 8 𝑧 ∈ V
2625snss 4286 . . . . . . 7 (𝑧 ∈ (𝐴 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝐴 ∪ {𝑧}))
2724, 26mpbir 221 . . . . . 6 𝑧 ∈ (𝐴 ∪ {𝑧})
28 ffvelrn 6313 . . . . . 6 ((𝑔:(𝐴 ∪ {𝑧})⟶𝐵𝑧 ∈ (𝐴 ∪ {𝑧})) → (𝑔𝑧) ∈ 𝐵)
2923, 27, 28sylancl 693 . . . . 5 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑔𝑧) ∈ 𝐵)
30 hashf1lem2.3 . . . . . . 7 (𝜑 → ¬ 𝑧𝐴)
3130adantr 481 . . . . . 6 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ¬ 𝑧𝐴)
32 df-ima 5087 . . . . . . . . 9 (𝑔𝐴) = ran (𝑔𝐴)
33 simprl 793 . . . . . . . . . 10 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑔𝐴) = 𝐹)
3433rneqd 5313 . . . . . . . . 9 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ran (𝑔𝐴) = ran 𝐹)
3532, 34syl5eq 2667 . . . . . . . 8 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑔𝐴) = ran 𝐹)
3635eleq2d 2684 . . . . . . 7 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ((𝑔𝑧) ∈ (𝑔𝐴) ↔ (𝑔𝑧) ∈ ran 𝐹))
37 simprr 795 . . . . . . . 8 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)
3827a1i 11 . . . . . . . 8 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝑧 ∈ (𝐴 ∪ {𝑧}))
39 ssun1 3754 . . . . . . . . 9 𝐴 ⊆ (𝐴 ∪ {𝑧})
4039a1i 11 . . . . . . . 8 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → 𝐴 ⊆ (𝐴 ∪ {𝑧}))
41 f1elima 6474 . . . . . . . 8 ((𝑔:(𝐴 ∪ {𝑧})–1-1𝐵𝑧 ∈ (𝐴 ∪ {𝑧}) ∧ 𝐴 ⊆ (𝐴 ∪ {𝑧})) → ((𝑔𝑧) ∈ (𝑔𝐴) ↔ 𝑧𝐴))
4237, 38, 40, 41syl3anc 1323 . . . . . . 7 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ((𝑔𝑧) ∈ (𝑔𝐴) ↔ 𝑧𝐴))
4336, 42bitr3d 270 . . . . . 6 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ((𝑔𝑧) ∈ ran 𝐹𝑧𝐴))
4431, 43mtbird 315 . . . . 5 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → ¬ (𝑔𝑧) ∈ ran 𝐹)
4529, 44eldifd 3566 . . . 4 ((𝜑 ∧ ((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)) → (𝑔𝑧) ∈ (𝐵 ∖ ran 𝐹))
4645ex 450 . . 3 (𝜑 → (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) → (𝑔𝑧) ∈ (𝐵 ∖ ran 𝐹)))
4721, 46syl5bi 232 . 2 (𝜑 → (𝑔 ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} → (𝑔𝑧) ∈ (𝐵 ∖ ran 𝐹)))
48 hashf1lem1.5 . . . . . . 7 (𝜑𝐹:𝐴1-1𝐵)
49 f1f 6058 . . . . . . 7 (𝐹:𝐴1-1𝐵𝐹:𝐴𝐵)
5048, 49syl 17 . . . . . 6 (𝜑𝐹:𝐴𝐵)
5150adantr 481 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴𝐵)
52 vex 3189 . . . . . . . 8 𝑥 ∈ V
5325, 52f1osn 6133 . . . . . . 7 {⟨𝑧, 𝑥⟩}:{𝑧}–1-1-onto→{𝑥}
54 f1of 6094 . . . . . . 7 ({⟨𝑧, 𝑥⟩}:{𝑧}–1-1-onto→{𝑥} → {⟨𝑧, 𝑥⟩}:{𝑧}⟶{𝑥})
5553, 54ax-mp 5 . . . . . 6 {⟨𝑧, 𝑥⟩}:{𝑧}⟶{𝑥}
56 eldifi 3710 . . . . . . . 8 (𝑥 ∈ (𝐵 ∖ ran 𝐹) → 𝑥𝐵)
5756adantl 482 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝑥𝐵)
5857snssd 4309 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {𝑥} ⊆ 𝐵)
59 fss 6013 . . . . . 6 (({⟨𝑧, 𝑥⟩}:{𝑧}⟶{𝑥} ∧ {𝑥} ⊆ 𝐵) → {⟨𝑧, 𝑥⟩}:{𝑧}⟶𝐵)
6055, 58, 59sylancr 694 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {⟨𝑧, 𝑥⟩}:{𝑧}⟶𝐵)
61 res0 5360 . . . . . . 7 (𝐹 ↾ ∅) = ∅
62 res0 5360 . . . . . . 7 ({⟨𝑧, 𝑥⟩} ↾ ∅) = ∅
6361, 62eqtr4i 2646 . . . . . 6 (𝐹 ↾ ∅) = ({⟨𝑧, 𝑥⟩} ↾ ∅)
64 disjsn 4216 . . . . . . . . 9 ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧𝐴)
6530, 64sylibr 224 . . . . . . . 8 (𝜑 → (𝐴 ∩ {𝑧}) = ∅)
6665adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐴 ∩ {𝑧}) = ∅)
6766reseq2d 5356 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = (𝐹 ↾ ∅))
6866reseq2d 5356 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ({⟨𝑧, 𝑥⟩} ↾ (𝐴 ∩ {𝑧})) = ({⟨𝑧, 𝑥⟩} ↾ ∅))
6963, 67, 683eqtr4a 2681 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({⟨𝑧, 𝑥⟩} ↾ (𝐴 ∩ {𝑧})))
70 fresaunres1 6034 . . . . 5 ((𝐹:𝐴𝐵 ∧ {⟨𝑧, 𝑥⟩}:{𝑧}⟶𝐵 ∧ (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({⟨𝑧, 𝑥⟩} ↾ (𝐴 ∩ {𝑧}))) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹)
7151, 60, 69, 70syl3anc 1323 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹)
72 f1f1orn 6105 . . . . . . . . 9 (𝐹:𝐴1-1𝐵𝐹:𝐴1-1-onto→ran 𝐹)
7348, 72syl 17 . . . . . . . 8 (𝜑𝐹:𝐴1-1-onto→ran 𝐹)
7473adantr 481 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴1-1-onto→ran 𝐹)
7553a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {⟨𝑧, 𝑥⟩}:{𝑧}–1-1-onto→{𝑥})
76 eldifn 3711 . . . . . . . . 9 (𝑥 ∈ (𝐵 ∖ ran 𝐹) → ¬ 𝑥 ∈ ran 𝐹)
7776adantl 482 . . . . . . . 8 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ¬ 𝑥 ∈ ran 𝐹)
78 disjsn 4216 . . . . . . . 8 ((ran 𝐹 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹)
7977, 78sylibr 224 . . . . . . 7 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∩ {𝑥}) = ∅)
80 f1oun 6113 . . . . . . 7 (((𝐹:𝐴1-1-onto→ran 𝐹 ∧ {⟨𝑧, 𝑥⟩}:{𝑧}–1-1-onto→{𝑥}) ∧ ((𝐴 ∩ {𝑧}) = ∅ ∧ (ran 𝐹 ∩ {𝑥}) = ∅)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1-onto→(ran 𝐹 ∪ {𝑥}))
8174, 75, 66, 79, 80syl22anc 1324 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1-onto→(ran 𝐹 ∪ {𝑥}))
82 f1of1 6093 . . . . . 6 ((𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1-onto→(ran 𝐹 ∪ {𝑥}) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥}))
8381, 82syl 17 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥}))
84 frn 6010 . . . . . . 7 (𝐹:𝐴𝐵 → ran 𝐹𝐵)
8551, 84syl 17 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ran 𝐹𝐵)
8685, 58unssd 3767 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵)
87 f1ss 6063 . . . . 5 (((𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥}) ∧ (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵)
8883, 86, 87syl2anc 692 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵)
89 fex 6444 . . . . . . . 8 ((𝐹:𝐴𝐵𝐴 ∈ Fin) → 𝐹 ∈ V)
9050, 4, 89syl2anc 692 . . . . . . 7 (𝜑𝐹 ∈ V)
9190adantr 481 . . . . . 6 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹 ∈ V)
92 snex 4869 . . . . . 6 {⟨𝑧, 𝑥⟩} ∈ V
93 unexg 6912 . . . . . 6 ((𝐹 ∈ V ∧ {⟨𝑧, 𝑥⟩} ∈ V) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ V)
9491, 92, 93sylancl 693 . . . . 5 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ V)
95 reseq1 5350 . . . . . . . 8 (𝑓 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) → (𝑓𝐴) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴))
9695eqeq1d 2623 . . . . . . 7 (𝑓 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) → ((𝑓𝐴) = 𝐹 ↔ ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹))
97 f1eq1 6053 . . . . . . 7 (𝑓 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) → (𝑓:(𝐴 ∪ {𝑧})–1-1𝐵 ↔ (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵))
9896, 97anbi12d 746 . . . . . 6 (𝑓 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) → (((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵) ↔ (((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵)))
9998elabg 3334 . . . . 5 ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ V → ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ↔ (((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵)))
10094, 99syl 17 . . . 4 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ↔ (((𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1𝐵)))
10171, 88, 100mpbir2and 956 . . 3 ((𝜑𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)})
102101ex 450 . 2 (𝜑 → (𝑥 ∈ (𝐵 ∖ ran 𝐹) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)}))
10321anbi1i 730 . . 3 ((𝑔 ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) ↔ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)))
104 simprlr 802 . . . . . . 7 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔:(𝐴 ∪ {𝑧})–1-1𝐵)
105 f1fn 6059 . . . . . . 7 (𝑔:(𝐴 ∪ {𝑧})–1-1𝐵𝑔 Fn (𝐴 ∪ {𝑧}))
106104, 105syl 17 . . . . . 6 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔 Fn (𝐴 ∪ {𝑧}))
10781adantrl 751 . . . . . . 7 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1-onto→(ran 𝐹 ∪ {𝑥}))
108 f1ofn 6095 . . . . . . 7 ((𝐹 ∪ {⟨𝑧, 𝑥⟩}):(𝐴 ∪ {𝑧})–1-1-onto→(ran 𝐹 ∪ {𝑥}) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) Fn (𝐴 ∪ {𝑧}))
109107, 108syl 17 . . . . . 6 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {⟨𝑧, 𝑥⟩}) Fn (𝐴 ∪ {𝑧}))
110 eqfnfv 6267 . . . . . 6 ((𝑔 Fn (𝐴 ∪ {𝑧}) ∧ (𝐹 ∪ {⟨𝑧, 𝑥⟩}) Fn (𝐴 ∪ {𝑧})) → (𝑔 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦)))
111106, 109, 110syl2anc 692 . . . . 5 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦)))
112 fvres 6164 . . . . . . . . . . 11 (𝑦𝐴 → ((𝑔𝐴)‘𝑦) = (𝑔𝑦))
113112eqcomd 2627 . . . . . . . . . 10 (𝑦𝐴 → (𝑔𝑦) = ((𝑔𝐴)‘𝑦))
114 simprll 801 . . . . . . . . . . 11 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔𝐴) = 𝐹)
115114fveq1d 6150 . . . . . . . . . 10 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔𝐴)‘𝑦) = (𝐹𝑦))
116113, 115sylan9eqr 2677 . . . . . . . . 9 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → (𝑔𝑦) = (𝐹𝑦))
11748ad2antrr 761 . . . . . . . . . . 11 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → 𝐹:𝐴1-1𝐵)
118 f1fn 6059 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
119117, 118syl 17 . . . . . . . . . 10 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → 𝐹 Fn 𝐴)
12025, 52fnsn 5904 . . . . . . . . . . 11 {⟨𝑧, 𝑥⟩} Fn {𝑧}
121120a1i 11 . . . . . . . . . 10 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → {⟨𝑧, 𝑥⟩} Fn {𝑧})
12265ad2antrr 761 . . . . . . . . . 10 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → (𝐴 ∩ {𝑧}) = ∅)
123 simpr 477 . . . . . . . . . 10 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → 𝑦𝐴)
124 fvun1 6226 . . . . . . . . . 10 ((𝐹 Fn 𝐴 ∧ {⟨𝑧, 𝑥⟩} Fn {𝑧} ∧ ((𝐴 ∩ {𝑧}) = ∅ ∧ 𝑦𝐴)) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) = (𝐹𝑦))
125119, 121, 122, 123, 124syl112anc 1327 . . . . . . . . 9 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) = (𝐹𝑦))
126116, 125eqtr4d 2658 . . . . . . . 8 (((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦𝐴) → (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦))
127126ralrimiva 2960 . . . . . . 7 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ∀𝑦𝐴 (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦))
128127biantrurd 529 . . . . . 6 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ (∀𝑦𝐴 (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦))))
129 ralunb 3772 . . . . . 6 (∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ (∀𝑦𝐴 (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦)))
130128, 129syl6bbr 278 . . . . 5 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦)))
13125a1i 11 . . . . . . . 8 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑧 ∈ V)
13252a1i 11 . . . . . . . 8 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑥 ∈ V)
133 fdm 6008 . . . . . . . . . . . 12 (𝐹:𝐴𝐵 → dom 𝐹 = 𝐴)
13450, 133syl 17 . . . . . . . . . . 11 (𝜑 → dom 𝐹 = 𝐴)
135134eleq2d 2684 . . . . . . . . . 10 (𝜑 → (𝑧 ∈ dom 𝐹𝑧𝐴))
13630, 135mtbird 315 . . . . . . . . 9 (𝜑 → ¬ 𝑧 ∈ dom 𝐹)
137136adantr 481 . . . . . . . 8 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ¬ 𝑧 ∈ dom 𝐹)
138 fsnunfv 6407 . . . . . . . 8 ((𝑧 ∈ V ∧ 𝑥 ∈ V ∧ ¬ 𝑧 ∈ dom 𝐹) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧) = 𝑥)
139131, 132, 137, 138syl3anc 1323 . . . . . . 7 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧) = 𝑥)
140139eqeq2d 2631 . . . . . 6 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔𝑧) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧) ↔ (𝑔𝑧) = 𝑥))
141 fveq2 6148 . . . . . . . 8 (𝑦 = 𝑧 → (𝑔𝑦) = (𝑔𝑧))
142 fveq2 6148 . . . . . . . 8 (𝑦 = 𝑧 → ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧))
143141, 142eqeq12d 2636 . . . . . . 7 (𝑦 = 𝑧 → ((𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ (𝑔𝑧) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧)))
14425, 143ralsn 4193 . . . . . 6 (∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ (𝑔𝑧) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑧))
145 eqcom 2628 . . . . . 6 (𝑥 = (𝑔𝑧) ↔ (𝑔𝑧) = 𝑥)
146140, 144, 1453bitr4g 303 . . . . 5 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔𝑦) = ((𝐹 ∪ {⟨𝑧, 𝑥⟩})‘𝑦) ↔ 𝑥 = (𝑔𝑧)))
147111, 130, 1463bitr2d 296 . . . 4 ((𝜑 ∧ (((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↔ 𝑥 = (𝑔𝑧)))
148147ex 450 . . 3 (𝜑 → ((((𝑔𝐴) = 𝐹𝑔:(𝐴 ∪ {𝑧})–1-1𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↔ 𝑥 = (𝑔𝑧))))
149103, 148syl5bi 232 . 2 (𝜑 → ((𝑔 ∈ {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {⟨𝑧, 𝑥⟩}) ↔ 𝑥 = (𝑔𝑧))))
15013, 15, 47, 102, 149en3d 7936 1 (𝜑 → {𝑓 ∣ ((𝑓𝐴) = 𝐹𝑓:(𝐴 ∪ {𝑧})–1-1𝐵)} ≈ (𝐵 ∖ ran 𝐹))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  {cab 2607  wral 2907  Vcvv 3186  cdif 3552  cun 3553  cin 3554  wss 3555  c0 3891  {csn 4148  cop 4154   class class class wbr 4613  dom cdm 5074  ran crn 5075  cres 5076  cima 5077   Fn wfn 5842  wf 5843  1-1wf1 5844  1-1-ontowf1o 5846  cfv 5847  (class class class)co 6604  𝑚 cmap 7802  cen 7896  Fincfn 7899  1c1 9881   + caddc 9883  cle 10019  #chash 13057
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-reu 2914  df-rab 2916  df-v 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-oadd 7509  df-er 7687  df-map 7804  df-en 7900  df-fin 7903
This theorem is referenced by:  hashf1lem2  13178
  Copyright terms: Public domain W3C validator