Step | Hyp | Ref
| Expression |
1 | | f1f 6670 |
. . . . . 6
⊢ (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵) |
2 | 1 | adantl 482 |
. . . . 5
⊢ (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵) |
3 | | hashf1lem2.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) |
4 | | hashf1lem2.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ Fin) |
5 | | snfi 8834 |
. . . . . . 7
⊢ {𝑧} ∈ Fin |
6 | | unfi 8955 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
7 | 4, 5, 6 | sylancl 586 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
8 | 3, 7 | elmapd 8629 |
. . . . 5
⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑m (𝐴 ∪ {𝑧})) ↔ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)) |
9 | 2, 8 | syl5ibr 245 |
. . . 4
⊢ (𝜑 → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓 ∈ (𝐵 ↑m (𝐴 ∪ {𝑧})))) |
10 | 9 | abssdv 4002 |
. . 3
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ (𝐵 ↑m (𝐴 ∪ {𝑧}))) |
11 | | ovex 7308 |
. . 3
⊢ (𝐵 ↑m (𝐴 ∪ {𝑧})) ∈ V |
12 | | ssexg 5247 |
. . 3
⊢ (({𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ (𝐵 ↑m (𝐴 ∪ {𝑧})) ∧ (𝐵 ↑m (𝐴 ∪ {𝑧})) ∈ V) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ V) |
13 | 10, 11, 12 | sylancl 586 |
. 2
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ V) |
14 | | difexg 5251 |
. . 3
⊢ (𝐵 ∈ Fin → (𝐵 ∖ ran 𝐹) ∈ V) |
15 | 3, 14 | syl 17 |
. 2
⊢ (𝜑 → (𝐵 ∖ ran 𝐹) ∈ V) |
16 | | vex 3436 |
. . . 4
⊢ 𝑔 ∈ V |
17 | | reseq1 5885 |
. . . . . 6
⊢ (𝑓 = 𝑔 → (𝑓 ↾ 𝐴) = (𝑔 ↾ 𝐴)) |
18 | 17 | eqeq1d 2740 |
. . . . 5
⊢ (𝑓 = 𝑔 → ((𝑓 ↾ 𝐴) = 𝐹 ↔ (𝑔 ↾ 𝐴) = 𝐹)) |
19 | | f1eq1 6665 |
. . . . 5
⊢ (𝑓 = 𝑔 → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ↔ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) |
20 | 18, 19 | anbi12d 631 |
. . . 4
⊢ (𝑓 = 𝑔 → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵))) |
21 | 16, 20 | elab 3609 |
. . 3
⊢ (𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) |
22 | | f1f 6670 |
. . . . . . 7
⊢ (𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑔:(𝐴 ∪ {𝑧})⟶𝐵) |
23 | 22 | ad2antll 726 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑔:(𝐴 ∪ {𝑧})⟶𝐵) |
24 | | ssun2 4107 |
. . . . . . 7
⊢ {𝑧} ⊆ (𝐴 ∪ {𝑧}) |
25 | | vex 3436 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
26 | 25 | snss 4719 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝐴 ∪ {𝑧})) |
27 | 24, 26 | mpbir 230 |
. . . . . 6
⊢ 𝑧 ∈ (𝐴 ∪ {𝑧}) |
28 | | ffvelrn 6959 |
. . . . . 6
⊢ ((𝑔:(𝐴 ∪ {𝑧})⟶𝐵 ∧ 𝑧 ∈ (𝐴 ∪ {𝑧})) → (𝑔‘𝑧) ∈ 𝐵) |
29 | 23, 27, 28 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔‘𝑧) ∈ 𝐵) |
30 | | hashf1lem2.3 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
31 | 30 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ¬ 𝑧 ∈ 𝐴) |
32 | | df-ima 5602 |
. . . . . . . . 9
⊢ (𝑔 “ 𝐴) = ran (𝑔 ↾ 𝐴) |
33 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔 ↾ 𝐴) = 𝐹) |
34 | 33 | rneqd 5847 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ran (𝑔 ↾ 𝐴) = ran 𝐹) |
35 | 32, 34 | eqtrid 2790 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔 “ 𝐴) = ran 𝐹) |
36 | 35 | eleq2d 2824 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ (𝑔‘𝑧) ∈ ran 𝐹)) |
37 | | simprr 770 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) |
38 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑧 ∈ (𝐴 ∪ {𝑧})) |
39 | | ssun1 4106 |
. . . . . . . . 9
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝐴 ⊆ (𝐴 ∪ {𝑧})) |
41 | | f1elima 7136 |
. . . . . . . 8
⊢ ((𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 ∧ 𝑧 ∈ (𝐴 ∪ {𝑧}) ∧ 𝐴 ⊆ (𝐴 ∪ {𝑧})) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ 𝑧 ∈ 𝐴)) |
42 | 37, 38, 40, 41 | syl3anc 1370 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ 𝑧 ∈ 𝐴)) |
43 | 36, 42 | bitr3d 280 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐴)) |
44 | 31, 43 | mtbird 325 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ¬ (𝑔‘𝑧) ∈ ran 𝐹) |
45 | 29, 44 | eldifd 3898 |
. . . 4
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹)) |
46 | 45 | ex 413 |
. . 3
⊢ (𝜑 → (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹))) |
47 | 21, 46 | syl5bi 241 |
. 2
⊢ (𝜑 → (𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹))) |
48 | | hashf1lem1.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |
49 | | f1f 6670 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
51 | 50 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴⟶𝐵) |
52 | | vex 3436 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
53 | 25, 52 | f1osn 6756 |
. . . . . . 7
⊢
{〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥} |
54 | | f1of 6716 |
. . . . . . 7
⊢
({〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥} → {〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥}) |
55 | 53, 54 | ax-mp 5 |
. . . . . 6
⊢
{〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥} |
56 | | eldifi 4061 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ ran 𝐹) → 𝑥 ∈ 𝐵) |
57 | 56 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝑥 ∈ 𝐵) |
58 | 57 | snssd 4742 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {𝑥} ⊆ 𝐵) |
59 | | fss 6617 |
. . . . . 6
⊢
(({〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥} ∧ {𝑥} ⊆ 𝐵) → {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵) |
60 | 55, 58, 59 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵) |
61 | | res0 5895 |
. . . . . . 7
⊢ (𝐹 ↾ ∅) =
∅ |
62 | | res0 5895 |
. . . . . . 7
⊢
({〈𝑧, 𝑥〉} ↾ ∅) =
∅ |
63 | 61, 62 | eqtr4i 2769 |
. . . . . 6
⊢ (𝐹 ↾ ∅) =
({〈𝑧, 𝑥〉} ↾
∅) |
64 | | disjsn 4647 |
. . . . . . . . 9
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
65 | 30, 64 | sylibr 233 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
66 | 65 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐴 ∩ {𝑧}) = ∅) |
67 | 66 | reseq2d 5891 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = (𝐹 ↾ ∅)) |
68 | 66 | reseq2d 5891 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ ∅)) |
69 | 63, 67, 68 | 3eqtr4a 2804 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧}))) |
70 | | fresaunres1 6647 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵 ∧ (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧}))) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹) |
71 | 51, 60, 69, 70 | syl3anc 1370 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹) |
72 | | f1f1orn 6727 |
. . . . . . . . 9
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
73 | 48, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
74 | 73 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴–1-1-onto→ran
𝐹) |
75 | 53 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥}) |
76 | | eldifn 4062 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ ran 𝐹) → ¬ 𝑥 ∈ ran 𝐹) |
77 | 76 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ¬ 𝑥 ∈ ran 𝐹) |
78 | | disjsn 4647 |
. . . . . . . 8
⊢ ((ran
𝐹 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹) |
79 | 77, 78 | sylibr 233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∩ {𝑥}) = ∅) |
80 | | f1oun 6735 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1-onto→ran
𝐹 ∧ {〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥}) ∧ ((𝐴 ∩ {𝑧}) = ∅ ∧ (ran 𝐹 ∩ {𝑥}) = ∅)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
81 | 74, 75, 66, 79, 80 | syl22anc 836 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
82 | | f1of1 6715 |
. . . . . 6
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥}) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥})) |
83 | 81, 82 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥})) |
84 | 51 | frnd 6608 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ran 𝐹 ⊆ 𝐵) |
85 | 84, 58 | unssd 4120 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵) |
86 | | f1ss 6676 |
. . . . 5
⊢ (((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥}) ∧ (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵) |
87 | 83, 85, 86 | syl2anc 584 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵) |
88 | 50, 4 | fexd 7103 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ V) |
89 | 88 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹 ∈ V) |
90 | | snex 5354 |
. . . . . 6
⊢
{〈𝑧, 𝑥〉} ∈
V |
91 | | unexg 7599 |
. . . . . 6
⊢ ((𝐹 ∈ V ∧ {〈𝑧, 𝑥〉} ∈ V) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V) |
92 | 89, 90, 91 | sylancl 586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V) |
93 | | reseq1 5885 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (𝑓 ↾ 𝐴) = ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴)) |
94 | 93 | eqeq1d 2740 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → ((𝑓 ↾ 𝐴) = 𝐹 ↔ ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹)) |
95 | | f1eq1 6665 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ↔ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵)) |
96 | 94, 95 | anbi12d 631 |
. . . . . 6
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
97 | 96 | elabg 3607 |
. . . . 5
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
98 | 92, 97 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
99 | 71, 87, 98 | mpbir2and 710 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) |
100 | 99 | ex 413 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ ran 𝐹) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) |
101 | 21 | anbi1i 624 |
. . 3
⊢ ((𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) ↔ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) |
102 | | simprlr 777 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) |
103 | | f1fn 6671 |
. . . . . . 7
⊢ (𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑔 Fn (𝐴 ∪ {𝑧})) |
104 | 102, 103 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔 Fn (𝐴 ∪ {𝑧})) |
105 | 81 | adantrl 713 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
106 | | f1ofn 6717 |
. . . . . . 7
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥}) → (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) |
107 | 105, 106 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) |
108 | | eqfnfv 6909 |
. . . . . 6
⊢ ((𝑔 Fn (𝐴 ∪ {𝑧}) ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
109 | 104, 107,
108 | syl2anc 584 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
110 | | fvres 6793 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((𝑔 ↾ 𝐴)‘𝑦) = (𝑔‘𝑦)) |
111 | 110 | eqcomd 2744 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (𝑔‘𝑦) = ((𝑔 ↾ 𝐴)‘𝑦)) |
112 | | simprll 776 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 ↾ 𝐴) = 𝐹) |
113 | 112 | fveq1d 6776 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
114 | 111, 113 | sylan9eqr 2800 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) = (𝐹‘𝑦)) |
115 | 48 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝐹:𝐴–1-1→𝐵) |
116 | | f1fn 6671 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
117 | 115, 116 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝐹 Fn 𝐴) |
118 | 25, 52 | fnsn 6492 |
. . . . . . . . . . 11
⊢
{〈𝑧, 𝑥〉} Fn {𝑧} |
119 | 118 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → {〈𝑧, 𝑥〉} Fn {𝑧}) |
120 | 65 | ad2antrr 723 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝐴 ∩ {𝑧}) = ∅) |
121 | | simpr 485 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
122 | 117, 119,
120, 121 | fvun1d 6861 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) = (𝐹‘𝑦)) |
123 | 114, 122 | eqtr4d 2781 |
. . . . . . . 8
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)) |
124 | 123 | ralrimiva 3103 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)) |
125 | 124 | biantrurd 533 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)))) |
126 | | ralunb 4125 |
. . . . . 6
⊢
(∀𝑦 ∈
(𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
127 | 125, 126 | bitr4di 289 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
128 | 50 | fdmd 6611 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐴) |
129 | 128 | eleq2d 2824 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴)) |
130 | 30, 129 | mtbird 325 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑧 ∈ dom 𝐹) |
131 | 130 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ¬ 𝑧 ∈ dom 𝐹) |
132 | | fsnunfv 7059 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝑥 ∈ V ∧ ¬ 𝑧 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) = 𝑥) |
133 | 25, 52, 131, 132 | mp3an12i 1464 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) = 𝑥) |
134 | 133 | eqeq2d 2749 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) ↔ (𝑔‘𝑧) = 𝑥)) |
135 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑔‘𝑦) = (𝑔‘𝑧)) |
136 | | fveq2 6774 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧)) |
137 | 135, 136 | eqeq12d 2754 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧))) |
138 | 25, 137 | ralsn 4617 |
. . . . . 6
⊢
(∀𝑦 ∈
{𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧)) |
139 | | eqcom 2745 |
. . . . . 6
⊢ (𝑥 = (𝑔‘𝑧) ↔ (𝑔‘𝑧) = 𝑥) |
140 | 134, 138,
139 | 3bitr4g 314 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ 𝑥 = (𝑔‘𝑧))) |
141 | 109, 127,
140 | 3bitr2d 307 |
. . . 4
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧))) |
142 | 141 | ex 413 |
. . 3
⊢ (𝜑 → ((((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧)))) |
143 | 101, 142 | syl5bi 241 |
. 2
⊢ (𝜑 → ((𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧)))) |
144 | 13, 15, 47, 100, 143 | en3d 8777 |
1
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹)) |