Step | Hyp | Ref
| Expression |
1 | | f1f 6014 |
. . . . . 6
⊢ (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵) |
2 | 1 | adantl 481 |
. . . . 5
⊢ (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓:(𝐴 ∪ {𝑧})⟶𝐵) |
3 | | hashf1lem2.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ Fin) |
4 | | hashf1lem2.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ Fin) |
5 | | snfi 7923 |
. . . . . . 7
⊢ {𝑧} ∈ Fin |
6 | | unfi 8112 |
. . . . . . 7
⊢ ((𝐴 ∈ Fin ∧ {𝑧} ∈ Fin) → (𝐴 ∪ {𝑧}) ∈ Fin) |
7 | 4, 5, 6 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → (𝐴 ∪ {𝑧}) ∈ Fin) |
8 | 3, 7 | elmapd 7758 |
. . . . 5
⊢ (𝜑 → (𝑓 ∈ (𝐵 ↑𝑚 (𝐴 ∪ {𝑧})) ↔ 𝑓:(𝐴 ∪ {𝑧})⟶𝐵)) |
9 | 2, 8 | syl5ibr 235 |
. . . 4
⊢ (𝜑 → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) → 𝑓 ∈ (𝐵 ↑𝑚 (𝐴 ∪ {𝑧})))) |
10 | 9 | abssdv 3639 |
. . 3
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ (𝐵 ↑𝑚 (𝐴 ∪ {𝑧}))) |
11 | | ovex 6577 |
. . 3
⊢ (𝐵 ↑𝑚
(𝐴 ∪ {𝑧})) ∈ V |
12 | | ssexg 4732 |
. . 3
⊢ (({𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ⊆ (𝐵 ↑𝑚 (𝐴 ∪ {𝑧})) ∧ (𝐵 ↑𝑚 (𝐴 ∪ {𝑧})) ∈ V) → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ V) |
13 | 10, 11, 12 | sylancl 693 |
. 2
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∈ V) |
14 | | difexg 4735 |
. . 3
⊢ (𝐵 ∈ Fin → (𝐵 ∖ ran 𝐹) ∈ V) |
15 | 3, 14 | syl 17 |
. 2
⊢ (𝜑 → (𝐵 ∖ ran 𝐹) ∈ V) |
16 | | vex 3176 |
. . . 4
⊢ 𝑔 ∈ V |
17 | | reseq1 5311 |
. . . . . 6
⊢ (𝑓 = 𝑔 → (𝑓 ↾ 𝐴) = (𝑔 ↾ 𝐴)) |
18 | 17 | eqeq1d 2612 |
. . . . 5
⊢ (𝑓 = 𝑔 → ((𝑓 ↾ 𝐴) = 𝐹 ↔ (𝑔 ↾ 𝐴) = 𝐹)) |
19 | | f1eq1 6009 |
. . . . 5
⊢ (𝑓 = 𝑔 → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ↔ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) |
20 | 18, 19 | anbi12d 743 |
. . . 4
⊢ (𝑓 = 𝑔 → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵))) |
21 | 16, 20 | elab 3319 |
. . 3
⊢ (𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) |
22 | | f1f 6014 |
. . . . . . 7
⊢ (𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑔:(𝐴 ∪ {𝑧})⟶𝐵) |
23 | 22 | ad2antll 761 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑔:(𝐴 ∪ {𝑧})⟶𝐵) |
24 | | ssun2 3739 |
. . . . . . 7
⊢ {𝑧} ⊆ (𝐴 ∪ {𝑧}) |
25 | | vex 3176 |
. . . . . . . 8
⊢ 𝑧 ∈ V |
26 | 25 | snss 4259 |
. . . . . . 7
⊢ (𝑧 ∈ (𝐴 ∪ {𝑧}) ↔ {𝑧} ⊆ (𝐴 ∪ {𝑧})) |
27 | 24, 26 | mpbir 220 |
. . . . . 6
⊢ 𝑧 ∈ (𝐴 ∪ {𝑧}) |
28 | | ffvelrn 6265 |
. . . . . 6
⊢ ((𝑔:(𝐴 ∪ {𝑧})⟶𝐵 ∧ 𝑧 ∈ (𝐴 ∪ {𝑧})) → (𝑔‘𝑧) ∈ 𝐵) |
29 | 23, 27, 28 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔‘𝑧) ∈ 𝐵) |
30 | | hashf1lem2.3 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑧 ∈ 𝐴) |
31 | 30 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ¬ 𝑧 ∈ 𝐴) |
32 | | df-ima 5051 |
. . . . . . . . 9
⊢ (𝑔 “ 𝐴) = ran (𝑔 ↾ 𝐴) |
33 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔 ↾ 𝐴) = 𝐹) |
34 | 33 | rneqd 5274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ran (𝑔 ↾ 𝐴) = ran 𝐹) |
35 | 32, 34 | syl5eq 2656 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔 “ 𝐴) = ran 𝐹) |
36 | 35 | eleq2d 2673 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ (𝑔‘𝑧) ∈ ran 𝐹)) |
37 | | simprr 792 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) |
38 | 27 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝑧 ∈ (𝐴 ∪ {𝑧})) |
39 | | ssun1 3738 |
. . . . . . . . 9
⊢ 𝐴 ⊆ (𝐴 ∪ {𝑧}) |
40 | 39 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → 𝐴 ⊆ (𝐴 ∪ {𝑧})) |
41 | | f1elima 6421 |
. . . . . . . 8
⊢ ((𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 ∧ 𝑧 ∈ (𝐴 ∪ {𝑧}) ∧ 𝐴 ⊆ (𝐴 ∪ {𝑧})) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ 𝑧 ∈ 𝐴)) |
42 | 37, 38, 40, 41 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ (𝑔 “ 𝐴) ↔ 𝑧 ∈ 𝐴)) |
43 | 36, 42 | bitr3d 269 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ((𝑔‘𝑧) ∈ ran 𝐹 ↔ 𝑧 ∈ 𝐴)) |
44 | 31, 43 | mtbird 314 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → ¬ (𝑔‘𝑧) ∈ ran 𝐹) |
45 | 29, 44 | eldifd 3551 |
. . . 4
⊢ ((𝜑 ∧ ((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵)) → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹)) |
46 | 45 | ex 449 |
. . 3
⊢ (𝜑 → (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹))) |
47 | 21, 46 | syl5bi 231 |
. 2
⊢ (𝜑 → (𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} → (𝑔‘𝑧) ∈ (𝐵 ∖ ran 𝐹))) |
48 | | hashf1lem1.5 |
. . . . . . 7
⊢ (𝜑 → 𝐹:𝐴–1-1→𝐵) |
49 | | f1f 6014 |
. . . . . . 7
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴⟶𝐵) |
50 | 48, 49 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
51 | 50 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴⟶𝐵) |
52 | | vex 3176 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
53 | 25, 52 | f1osn 6088 |
. . . . . . 7
⊢
{〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥} |
54 | | f1of 6050 |
. . . . . . 7
⊢
({〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥} → {〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥}) |
55 | 53, 54 | ax-mp 5 |
. . . . . 6
⊢
{〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥} |
56 | | eldifi 3694 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝐵 ∖ ran 𝐹) → 𝑥 ∈ 𝐵) |
57 | 56 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝑥 ∈ 𝐵) |
58 | 57 | snssd 4281 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {𝑥} ⊆ 𝐵) |
59 | | fss 5969 |
. . . . . 6
⊢
(({〈𝑧, 𝑥〉}:{𝑧}⟶{𝑥} ∧ {𝑥} ⊆ 𝐵) → {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵) |
60 | 55, 58, 59 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵) |
61 | | res0 5321 |
. . . . . . 7
⊢ (𝐹 ↾ ∅) =
∅ |
62 | | res0 5321 |
. . . . . . 7
⊢
({〈𝑧, 𝑥〉} ↾ ∅) =
∅ |
63 | 61, 62 | eqtr4i 2635 |
. . . . . 6
⊢ (𝐹 ↾ ∅) =
({〈𝑧, 𝑥〉} ↾
∅) |
64 | | disjsn 4192 |
. . . . . . . . 9
⊢ ((𝐴 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝐴) |
65 | 30, 64 | sylibr 223 |
. . . . . . . 8
⊢ (𝜑 → (𝐴 ∩ {𝑧}) = ∅) |
66 | 65 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐴 ∩ {𝑧}) = ∅) |
67 | 66 | reseq2d 5317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = (𝐹 ↾ ∅)) |
68 | 66 | reseq2d 5317 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ ∅)) |
69 | 63, 67, 68 | 3eqtr4a 2670 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧}))) |
70 | | fresaunres1 5990 |
. . . . 5
⊢ ((𝐹:𝐴⟶𝐵 ∧ {〈𝑧, 𝑥〉}:{𝑧}⟶𝐵 ∧ (𝐹 ↾ (𝐴 ∩ {𝑧})) = ({〈𝑧, 𝑥〉} ↾ (𝐴 ∩ {𝑧}))) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹) |
71 | 51, 60, 69, 70 | syl3anc 1318 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹) |
72 | | f1f1orn 6061 |
. . . . . . . . 9
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
73 | 48, 72 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐴–1-1-onto→ran
𝐹) |
74 | 73 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹:𝐴–1-1-onto→ran
𝐹) |
75 | 53 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → {〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥}) |
76 | | eldifn 3695 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝐵 ∖ ran 𝐹) → ¬ 𝑥 ∈ ran 𝐹) |
77 | 76 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ¬ 𝑥 ∈ ran 𝐹) |
78 | | disjsn 4192 |
. . . . . . . 8
⊢ ((ran
𝐹 ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ ran 𝐹) |
79 | 77, 78 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∩ {𝑥}) = ∅) |
80 | | f1oun 6069 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1-onto→ran
𝐹 ∧ {〈𝑧, 𝑥〉}:{𝑧}–1-1-onto→{𝑥}) ∧ ((𝐴 ∩ {𝑧}) = ∅ ∧ (ran 𝐹 ∩ {𝑥}) = ∅)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
81 | 74, 75, 66, 79, 80 | syl22anc 1319 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
82 | | f1of1 6049 |
. . . . . 6
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥}) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥})) |
83 | 81, 82 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥})) |
84 | | frn 5966 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ 𝐵) |
85 | 51, 84 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ran 𝐹 ⊆ 𝐵) |
86 | 85, 58 | unssd 3751 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵) |
87 | | f1ss 6019 |
. . . . 5
⊢ (((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→(ran 𝐹 ∪ {𝑥}) ∧ (ran 𝐹 ∪ {𝑥}) ⊆ 𝐵) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵) |
88 | 83, 86, 87 | syl2anc 691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵) |
89 | | fex 6394 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ Fin) → 𝐹 ∈ V) |
90 | 50, 4, 89 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → 𝐹 ∈ V) |
91 | 90 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → 𝐹 ∈ V) |
92 | | snex 4835 |
. . . . . 6
⊢
{〈𝑧, 𝑥〉} ∈
V |
93 | | unexg 6857 |
. . . . . 6
⊢ ((𝐹 ∈ V ∧ {〈𝑧, 𝑥〉} ∈ V) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V) |
94 | 91, 92, 93 | sylancl 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V) |
95 | | reseq1 5311 |
. . . . . . . 8
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (𝑓 ↾ 𝐴) = ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴)) |
96 | 95 | eqeq1d 2612 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → ((𝑓 ↾ 𝐴) = 𝐹 ↔ ((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹)) |
97 | | f1eq1 6009 |
. . . . . . 7
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵 ↔ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵)) |
98 | 96, 97 | anbi12d 743 |
. . . . . 6
⊢ (𝑓 = (𝐹 ∪ {〈𝑧, 𝑥〉}) → (((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵) ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
99 | 98 | elabg 3320 |
. . . . 5
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ V → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
100 | 94, 99 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → ((𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ↔ (((𝐹 ∪ {〈𝑧, 𝑥〉}) ↾ 𝐴) = 𝐹 ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1→𝐵))) |
101 | 71, 88, 100 | mpbir2and 959 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)}) |
102 | 101 | ex 449 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐵 ∖ ran 𝐹) → (𝐹 ∪ {〈𝑧, 𝑥〉}) ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)})) |
103 | 21 | anbi1i 727 |
. . 3
⊢ ((𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) ↔ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) |
104 | | simprlr 799 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) |
105 | | f1fn 6015 |
. . . . . . 7
⊢ (𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵 → 𝑔 Fn (𝐴 ∪ {𝑧})) |
106 | 104, 105 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑔 Fn (𝐴 ∪ {𝑧})) |
107 | 81 | adantrl 748 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥})) |
108 | | f1ofn 6051 |
. . . . . . 7
⊢ ((𝐹 ∪ {〈𝑧, 𝑥〉}):(𝐴 ∪ {𝑧})–1-1-onto→(ran
𝐹 ∪ {𝑥}) → (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) |
109 | 107, 108 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) |
110 | | eqfnfv 6219 |
. . . . . 6
⊢ ((𝑔 Fn (𝐴 ∪ {𝑧}) ∧ (𝐹 ∪ {〈𝑧, 𝑥〉}) Fn (𝐴 ∪ {𝑧})) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
111 | 106, 109,
110 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
112 | | fvres 6117 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ 𝐴 → ((𝑔 ↾ 𝐴)‘𝑦) = (𝑔‘𝑦)) |
113 | 112 | eqcomd 2616 |
. . . . . . . . . 10
⊢ (𝑦 ∈ 𝐴 → (𝑔‘𝑦) = ((𝑔 ↾ 𝐴)‘𝑦)) |
114 | | simprll 798 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 ↾ 𝐴) = 𝐹) |
115 | 114 | fveq1d 6105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔 ↾ 𝐴)‘𝑦) = (𝐹‘𝑦)) |
116 | 113, 115 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) = (𝐹‘𝑦)) |
117 | 48 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝐹:𝐴–1-1→𝐵) |
118 | | f1fn 6015 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴–1-1→𝐵 → 𝐹 Fn 𝐴) |
119 | 117, 118 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝐹 Fn 𝐴) |
120 | 25, 52 | fnsn 5860 |
. . . . . . . . . . 11
⊢
{〈𝑧, 𝑥〉} Fn {𝑧} |
121 | 120 | a1i 11 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → {〈𝑧, 𝑥〉} Fn {𝑧}) |
122 | 65 | ad2antrr 758 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝐴 ∩ {𝑧}) = ∅) |
123 | | simpr 476 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ 𝐴) |
124 | | fvun1 6179 |
. . . . . . . . . 10
⊢ ((𝐹 Fn 𝐴 ∧ {〈𝑧, 𝑥〉} Fn {𝑧} ∧ ((𝐴 ∩ {𝑧}) = ∅ ∧ 𝑦 ∈ 𝐴)) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) = (𝐹‘𝑦)) |
125 | 119, 121,
122, 123, 124 | syl112anc 1322 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) = (𝐹‘𝑦)) |
126 | 116, 125 | eqtr4d 2647 |
. . . . . . . 8
⊢ (((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) ∧ 𝑦 ∈ 𝐴) → (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)) |
127 | 126 | ralrimiva 2949 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)) |
128 | 127 | biantrurd 528 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦)))) |
129 | | ralunb 3756 |
. . . . . 6
⊢
(∀𝑦 ∈
(𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (∀𝑦 ∈ 𝐴 (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ∧ ∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
130 | 128, 129 | syl6bbr 277 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ ∀𝑦 ∈ (𝐴 ∪ {𝑧})(𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦))) |
131 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑧 ∈ V) |
132 | 52 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → 𝑥 ∈ V) |
133 | | fdm 5964 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴) |
134 | 50, 133 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝐹 = 𝐴) |
135 | 134 | eleq2d 2673 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑧 ∈ dom 𝐹 ↔ 𝑧 ∈ 𝐴)) |
136 | 30, 135 | mtbird 314 |
. . . . . . . . 9
⊢ (𝜑 → ¬ 𝑧 ∈ dom 𝐹) |
137 | 136 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ¬ 𝑧 ∈ dom 𝐹) |
138 | | fsnunfv 6358 |
. . . . . . . 8
⊢ ((𝑧 ∈ V ∧ 𝑥 ∈ V ∧ ¬ 𝑧 ∈ dom 𝐹) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) = 𝑥) |
139 | 131, 132,
137, 138 | syl3anc 1318 |
. . . . . . 7
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) = 𝑥) |
140 | 139 | eqeq2d 2620 |
. . . . . 6
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → ((𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧) ↔ (𝑔‘𝑧) = 𝑥)) |
141 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → (𝑔‘𝑦) = (𝑔‘𝑧)) |
142 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑦 = 𝑧 → ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧)) |
143 | 141, 142 | eqeq12d 2625 |
. . . . . . 7
⊢ (𝑦 = 𝑧 → ((𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧))) |
144 | 25, 143 | ralsn 4169 |
. . . . . 6
⊢
(∀𝑦 ∈
{𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ (𝑔‘𝑧) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑧)) |
145 | | eqcom 2617 |
. . . . . 6
⊢ (𝑥 = (𝑔‘𝑧) ↔ (𝑔‘𝑧) = 𝑥) |
146 | 140, 144,
145 | 3bitr4g 302 |
. . . . 5
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (∀𝑦 ∈ {𝑧} (𝑔‘𝑦) = ((𝐹 ∪ {〈𝑧, 𝑥〉})‘𝑦) ↔ 𝑥 = (𝑔‘𝑧))) |
147 | 111, 130,
146 | 3bitr2d 295 |
. . . 4
⊢ ((𝜑 ∧ (((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹))) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧))) |
148 | 147 | ex 449 |
. . 3
⊢ (𝜑 → ((((𝑔 ↾ 𝐴) = 𝐹 ∧ 𝑔:(𝐴 ∪ {𝑧})–1-1→𝐵) ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧)))) |
149 | 103, 148 | syl5bi 231 |
. 2
⊢ (𝜑 → ((𝑔 ∈ {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ∧ 𝑥 ∈ (𝐵 ∖ ran 𝐹)) → (𝑔 = (𝐹 ∪ {〈𝑧, 𝑥〉}) ↔ 𝑥 = (𝑔‘𝑧)))) |
150 | 13, 15, 47, 102, 149 | en3d 7878 |
1
⊢ (𝜑 → {𝑓 ∣ ((𝑓 ↾ 𝐴) = 𝐹 ∧ 𝑓:(𝐴 ∪ {𝑧})–1-1→𝐵)} ≈ (𝐵 ∖ ran 𝐹)) |