| Step | Hyp | Ref
| Expression |
| 1 | | cnvimass 6100 |
. . . . 5
⊢ (◡𝐹 “ {𝑥}) ⊆ dom 𝐹 |
| 2 | | dnnumch.f |
. . . . . . 7
⊢ 𝐹 = recs((𝑧 ∈ V ↦ (𝐺‘(𝐴 ∖ ran 𝑧)))) |
| 3 | 2 | tfr1 8437 |
. . . . . 6
⊢ 𝐹 Fn On |
| 4 | 3 | fndmi 6672 |
. . . . 5
⊢ dom 𝐹 = On |
| 5 | 1, 4 | sseqtri 4032 |
. . . 4
⊢ (◡𝐹 “ {𝑥}) ⊆ On |
| 6 | | dnnumch.a |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 7 | | dnnumch.g |
. . . . . . 7
⊢ (𝜑 → ∀𝑦 ∈ 𝒫 𝐴(𝑦 ≠ ∅ → (𝐺‘𝑦) ∈ 𝑦)) |
| 8 | 2, 6, 7 | dnnumch2 43057 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ran 𝐹) |
| 9 | 8 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ran 𝐹) |
| 10 | | inisegn0 6116 |
. . . . 5
⊢ (𝑥 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑥}) ≠ ∅) |
| 11 | 9, 10 | sylib 218 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (◡𝐹 “ {𝑥}) ≠ ∅) |
| 12 | | oninton 7815 |
. . . 4
⊢ (((◡𝐹 “ {𝑥}) ⊆ On ∧ (◡𝐹 “ {𝑥}) ≠ ∅) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
| 13 | 5, 11, 12 | sylancr 587 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑥}) ∈ On) |
| 14 | 13 | fmpttd 7135 |
. 2
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On) |
| 15 | 2, 6, 7 | dnnumch3lem 43058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
| 16 | 15 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ∩ (◡𝐹 “ {𝑣})) |
| 17 | 2, 6, 7 | dnnumch3lem 43058 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
| 18 | 17 | adantrl 716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) = ∩ (◡𝐹 “ {𝑤})) |
| 19 | 16, 18 | eqeq12d 2753 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) ↔ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}))) |
| 20 | | fveq2 6906 |
. . . . . . 7
⊢ (∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
| 21 | 20 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = (𝐹‘∩ (◡𝐹 “ {𝑤}))) |
| 22 | | cnvimass 6100 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑣}) ⊆ dom 𝐹 |
| 23 | 22, 4 | sseqtri 4032 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑣}) ⊆ On |
| 24 | 8 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → 𝑣 ∈ ran 𝐹) |
| 25 | | inisegn0 6116 |
. . . . . . . . . . 11
⊢ (𝑣 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑣}) ≠ ∅) |
| 26 | 24, 25 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (◡𝐹 “ {𝑣}) ≠ ∅) |
| 27 | | onint 7810 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑣}) ⊆ On ∧ (◡𝐹 “ {𝑣}) ≠ ∅) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
| 28 | 23, 26, 27 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣})) |
| 29 | | fniniseg 7080 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣))) |
| 30 | 3, 29 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) ↔ (∩
(◡𝐹 “ {𝑣}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣)) |
| 31 | 30 | simprbi 496 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑣}) ∈ (◡𝐹 “ {𝑣}) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
| 32 | 28, 31 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑣 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
| 33 | 32 | adantrr 717 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
| 34 | 33 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑣})) = 𝑣) |
| 35 | | cnvimass 6100 |
. . . . . . . . . . 11
⊢ (◡𝐹 “ {𝑤}) ⊆ dom 𝐹 |
| 36 | 35, 4 | sseqtri 4032 |
. . . . . . . . . 10
⊢ (◡𝐹 “ {𝑤}) ⊆ On |
| 37 | 8 | sselda 3983 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → 𝑤 ∈ ran 𝐹) |
| 38 | | inisegn0 6116 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ ran 𝐹 ↔ (◡𝐹 “ {𝑤}) ≠ ∅) |
| 39 | 37, 38 | sylib 218 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (◡𝐹 “ {𝑤}) ≠ ∅) |
| 40 | | onint 7810 |
. . . . . . . . . 10
⊢ (((◡𝐹 “ {𝑤}) ⊆ On ∧ (◡𝐹 “ {𝑤}) ≠ ∅) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
| 41 | 36, 39, 40 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → ∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤})) |
| 42 | | fniniseg 7080 |
. . . . . . . . . . 11
⊢ (𝐹 Fn On → (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤))) |
| 43 | 3, 42 | ax-mp 5 |
. . . . . . . . . 10
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) ↔ (∩
(◡𝐹 “ {𝑤}) ∈ On ∧ (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤)) |
| 44 | 43 | simprbi 496 |
. . . . . . . . 9
⊢ (∩ (◡𝐹 “ {𝑤}) ∈ (◡𝐹 “ {𝑤}) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
| 45 | 41, 44 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝐴) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
| 46 | 45 | adantrl 716 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
| 47 | 46 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → (𝐹‘∩ (◡𝐹 “ {𝑤})) = 𝑤) |
| 48 | 21, 34, 47 | 3eqtr3d 2785 |
. . . . 5
⊢ (((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) ∧ ∩ (◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤})) → 𝑣 = 𝑤) |
| 49 | 48 | ex 412 |
. . . 4
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (∩
(◡𝐹 “ {𝑣}) = ∩ (◡𝐹 “ {𝑤}) → 𝑣 = 𝑤)) |
| 50 | 19, 49 | sylbid 240 |
. . 3
⊢ ((𝜑 ∧ (𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴)) → (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
| 51 | 50 | ralrimivva 3202 |
. 2
⊢ (𝜑 → ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤)) |
| 52 | | dff13 7275 |
. 2
⊢ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On ↔ ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴⟶On ∧ ∀𝑣 ∈ 𝐴 ∀𝑤 ∈ 𝐴 (((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑣) = ((𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥}))‘𝑤) → 𝑣 = 𝑤))) |
| 53 | 14, 51, 52 | sylanbrc 583 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ ∩ (◡𝐹 “ {𝑥})):𝐴–1-1→On) |