Step | Hyp | Ref
| Expression |
1 | | cnvimass 5933 |
. . . . 5
⊢ (◡𝐹 “ {𝑥}) ⊆ dom 𝐹 |
2 | | dnnumch.f |
. . . . . . 7
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) |
3 | 2 | tfr1 8074 |
. . . . . 6
⊢ 𝐹 Fn On |
4 | 3 | fndmi 6451 |
. . . . 5
⊢ dom 𝐹 = On |
5 | 1, 4 | sseqtri 3923 |
. . . 4
⊢ (◡𝐹 “ {𝑥}) ⊆ On |
6 | | dnnumch.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
7 | | dnnumch.g |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) |
8 | 2, 6, 7 | dnnumch2 40482 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) |
9 | 8 | sselda 3887 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran 𝐹) |
10 | | inisegn0 5945 |
. . . . 5
⊢ (𝑥 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑥}) ≠ ∅) |
11 | 9, 10 | sylib 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ {𝑥}) ≠ ∅) |
12 | | oninton 7546 |
. . . 4
⊢ (((◡𝐹 “ {𝑥}) ⊆ On ∧ (◡𝐹 “ {𝑥}) ≠ ∅) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
13 | 5, 11, 12 | sylancr 590 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
14 | 13 | fmpttd 6901 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On) |
15 | 2, 6, 7 | dnnumch3lem 40483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
16 | 15 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
17 | 2, 6, 7 | dnnumch3lem 40483 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
18 | 17 | adantrl 716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
19 | 16, 18 | eqeq12d 2755 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}))) |
20 | | fveq2 6686 |
. . . . . . 7
⊢ (∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
21 | 20 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
22 | | cnvimass 5933 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑣}) ⊆ dom 𝐹 |
23 | 22, 4 | sseqtri 3923 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑣}) ⊆ On |
24 | 8 | sselda 3887 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ ran 𝐹) |
25 | | inisegn0 5945 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑣}) ≠ ∅) |
26 | 24, 25 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (◡𝐹 “ {𝑣}) ≠ ∅) |
27 | | onint 7541 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑣}) ⊆ On ∧ (◡𝐹 “ {𝑣}) ≠ ∅) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
28 | 23, 26, 27 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
29 | | fniniseg 6849 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣))) |
30 | 3, 29 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)) |
31 | 30 | simprbi 500 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
32 | 28, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
33 | 32 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
34 | 33 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
35 | | cnvimass 5933 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑤}) ⊆ dom 𝐹 |
36 | 35, 4 | sseqtri 3923 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑤}) ⊆ On |
37 | 8 | sselda 3887 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ran 𝐹) |
38 | | inisegn0 5945 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑤}) ≠ ∅) |
39 | 37, 38 | sylib 221 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (◡𝐹 “ {𝑤}) ≠ ∅) |
40 | | onint 7541 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑤}) ⊆ On ∧ (◡𝐹 “ {𝑤}) ≠ ∅) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
41 | 36, 39, 40 | sylancr 590 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
42 | | fniniseg 6849 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤))) |
43 | 3, 42 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)) |
44 | 43 | simprbi 500 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
45 | 41, 44 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
46 | 45 | adantrl 716 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
47 | 46 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
48 | 21, 34, 47 | 3eqtr3d 2782 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → 𝑣 = 𝑤) |
49 | 48 | ex 416 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩
(◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → 𝑣 = 𝑤)) |
50 | 19, 49 | sylbid 243 |
. . 3
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
51 | 50 | ralrimivva 3104 |
. 2
⊢ (𝜑 → ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
52 | | dff13 7036 |
. 2
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On ∧ ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤))) |
53 | 14, 51, 52 | sylanbrc 586 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) |