Step | Hyp | Ref
| Expression |
1 | | cnvimass 5951 |
. . . . 5
⊢ (◡𝐹 “ {𝑥}) ⊆ dom 𝐹 |
2 | | dnnumch.f |
. . . . . . 7
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) |
3 | 2 | tfr1 8035 |
. . . . . 6
⊢ 𝐹 Fn On |
4 | | fndm 6457 |
. . . . . 6
⊢ (𝐹 Fn On → dom 𝐹 = On) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢ dom 𝐹 = On |
6 | 1, 5 | sseqtri 4005 |
. . . 4
⊢ (◡𝐹 “ {𝑥}) ⊆ On |
7 | | dnnumch.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
8 | | dnnumch.g |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) |
9 | 2, 7, 8 | dnnumch2 39652 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) |
10 | 9 | sselda 3969 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran 𝐹) |
11 | | inisegn0 5963 |
. . . . 5
⊢ (𝑥 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑥}) ≠ ∅) |
12 | 10, 11 | sylib 220 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ {𝑥}) ≠ ∅) |
13 | | oninton 7517 |
. . . 4
⊢ (((◡𝐹 “ {𝑥}) ⊆ On ∧ (◡𝐹 “ {𝑥}) ≠ ∅) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
14 | 6, 12, 13 | sylancr 589 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
15 | 14 | fmpttd 6881 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On) |
16 | 2, 7, 8 | dnnumch3lem 39653 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
17 | 16 | adantrr 715 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
18 | 2, 7, 8 | dnnumch3lem 39653 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
19 | 18 | adantrl 714 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
20 | 17, 19 | eqeq12d 2839 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}))) |
21 | | fveq2 6672 |
. . . . . . 7
⊢ (∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
22 | 21 | adantl 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
23 | | cnvimass 5951 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑣}) ⊆ dom 𝐹 |
24 | 23, 5 | sseqtri 4005 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑣}) ⊆ On |
25 | 9 | sselda 3969 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ ran 𝐹) |
26 | | inisegn0 5963 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑣}) ≠ ∅) |
27 | 25, 26 | sylib 220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (◡𝐹 “ {𝑣}) ≠ ∅) |
28 | | onint 7512 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑣}) ⊆ On ∧ (◡𝐹 “ {𝑣}) ≠ ∅) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
29 | 24, 27, 28 | sylancr 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
30 | | fniniseg 6832 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣))) |
31 | 3, 30 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)) |
32 | 31 | simprbi 499 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
33 | 29, 32 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
34 | 33 | adantrr 715 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
35 | 34 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
36 | | cnvimass 5951 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑤}) ⊆ dom 𝐹 |
37 | 36, 5 | sseqtri 4005 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑤}) ⊆ On |
38 | 9 | sselda 3969 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ran 𝐹) |
39 | | inisegn0 5963 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑤}) ≠ ∅) |
40 | 38, 39 | sylib 220 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (◡𝐹 “ {𝑤}) ≠ ∅) |
41 | | onint 7512 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑤}) ⊆ On ∧ (◡𝐹 “ {𝑤}) ≠ ∅) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
42 | 37, 40, 41 | sylancr 589 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
43 | | fniniseg 6832 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤))) |
44 | 3, 43 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)) |
45 | 44 | simprbi 499 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
46 | 42, 45 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
47 | 46 | adantrl 714 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
48 | 47 | adantr 483 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
49 | 22, 35, 48 | 3eqtr3d 2866 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → 𝑣 = 𝑤) |
50 | 49 | ex 415 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩
(◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → 𝑣 = 𝑤)) |
51 | 20, 50 | sylbid 242 |
. . 3
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
52 | 51 | ralrimivva 3193 |
. 2
⊢ (𝜑 → ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
53 | | dff13 7015 |
. 2
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On ∧ ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤))) |
54 | 15, 52, 53 | sylanbrc 585 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) |