Step | Hyp | Ref
| Expression |
1 | | f1ofn 6138 |
. . 3
⊢ (𝐹:𝐴–1-1-onto→𝐴 → 𝐹 Fn 𝐴) |
2 | 1 | ad2antrr 762 |
. 2
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
𝐹 Fn 𝐴) |
3 | | f1ofn 6138 |
. . 3
⊢ (𝐺:𝐴–1-1-onto→𝐴 → 𝐺 Fn 𝐴) |
4 | 3 | ad2antlr 763 |
. 2
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
𝐺 Fn 𝐴) |
5 | | 1onn 7719 |
. . . . . . . 8
⊢
1𝑜 ∈ ω |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) →
1𝑜 ∈ ω) |
7 | | simplrr 801 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → dom (𝐺 ∖ I ) = dom (𝐹 ∖ I )) |
8 | | simplrl 800 |
. . . . . . . . 9
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → dom (𝐹 ∖ I ) ≈
2𝑜) |
9 | | df-2o 7561 |
. . . . . . . . 9
⊢
2𝑜 = suc 1𝑜 |
10 | 8, 9 | syl6breq 4694 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → dom (𝐹 ∖ I ) ≈ suc
1𝑜) |
11 | 7, 10 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → dom (𝐺 ∖ I ) ≈ suc
1𝑜) |
12 | | simpr 477 |
. . . . . . 7
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → 𝑥 ∈ dom (𝐺 ∖ I )) |
13 | | dif1en 8193 |
. . . . . . 7
⊢
((1𝑜 ∈ ω ∧ dom (𝐺 ∖ I ) ≈ suc
1𝑜 ∧ 𝑥 ∈ dom (𝐺 ∖ I )) → (dom (𝐺 ∖ I ) ∖ {𝑥}) ≈
1𝑜) |
14 | 6, 11, 12, 13 | syl3anc 1326 |
. . . . . 6
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → (dom (𝐺 ∖ I ) ∖ {𝑥}) ≈
1𝑜) |
15 | | euen1b 8027 |
. . . . . . 7
⊢ ((dom
(𝐺 ∖ I ) ∖
{𝑥}) ≈
1𝑜 ↔ ∃!𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
16 | | eumo 2499 |
. . . . . . 7
⊢
(∃!𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) → ∃*𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
17 | 15, 16 | sylbi 207 |
. . . . . 6
⊢ ((dom
(𝐺 ∖ I ) ∖
{𝑥}) ≈
1𝑜 → ∃*𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
18 | 14, 17 | syl 17 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) →
∃*𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
19 | | f1omvdmvd 17863 |
. . . . . . . . 9
⊢ ((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝑥 ∈ dom (𝐹 ∖ I )) → (𝐹‘𝑥) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥})) |
20 | 19 | ex 450 |
. . . . . . . 8
⊢ (𝐹:𝐴–1-1-onto→𝐴 → (𝑥 ∈ dom (𝐹 ∖ I ) → (𝐹‘𝑥) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥}))) |
21 | 20 | ad2antrr 762 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
(𝑥 ∈ dom (𝐹 ∖ I ) → (𝐹‘𝑥) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥}))) |
22 | | eleq2 2690 |
. . . . . . . 8
⊢ (dom
(𝐺 ∖ I ) = dom (𝐹 ∖ I ) → (𝑥 ∈ dom (𝐺 ∖ I ) ↔ 𝑥 ∈ dom (𝐹 ∖ I ))) |
23 | 22 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
(𝑥 ∈ dom (𝐺 ∖ I ) ↔ 𝑥 ∈ dom (𝐹 ∖ I ))) |
24 | | difeq1 3721 |
. . . . . . . . 9
⊢ (dom
(𝐺 ∖ I ) = dom (𝐹 ∖ I ) → (dom (𝐺 ∖ I ) ∖ {𝑥}) = (dom (𝐹 ∖ I ) ∖ {𝑥})) |
25 | 24 | eleq2d 2687 |
. . . . . . . 8
⊢ (dom
(𝐺 ∖ I ) = dom (𝐹 ∖ I ) → ((𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ↔ (𝐹‘𝑥) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥}))) |
26 | 25 | ad2antll 765 |
. . . . . . 7
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
((𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ↔ (𝐹‘𝑥) ∈ (dom (𝐹 ∖ I ) ∖ {𝑥}))) |
27 | 21, 23, 26 | 3imtr4d 283 |
. . . . . 6
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
(𝑥 ∈ dom (𝐺 ∖ I ) → (𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}))) |
28 | 27 | imp 445 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → (𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
29 | | simplr 792 |
. . . . . 6
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
𝐺:𝐴–1-1-onto→𝐴) |
30 | | f1omvdmvd 17863 |
. . . . . 6
⊢ ((𝐺:𝐴–1-1-onto→𝐴 ∧ 𝑥 ∈ dom (𝐺 ∖ I )) → (𝐺‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
31 | 29, 30 | sylan 488 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → (𝐺‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥})) |
32 | | fvex 6201 |
. . . . . . 7
⊢ (𝐹‘𝑥) ∈ V |
33 | | fvex 6201 |
. . . . . . 7
⊢ (𝐺‘𝑥) ∈ V |
34 | 32, 33 | pm3.2i 471 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ V ∧ (𝐺‘𝑥) ∈ V) |
35 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ↔ (𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}))) |
36 | | eleq1 2689 |
. . . . . . 7
⊢ (𝑦 = (𝐺‘𝑥) → (𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ↔ (𝐺‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}))) |
37 | 35, 36 | moi 3389 |
. . . . . 6
⊢ ((((𝐹‘𝑥) ∈ V ∧ (𝐺‘𝑥) ∈ V) ∧ ∃*𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ∧ ((𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ∧ (𝐺‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}))) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
38 | 34, 37 | mp3an1 1411 |
. . . . 5
⊢
((∃*𝑦 𝑦 ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ∧ ((𝐹‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}) ∧ (𝐺‘𝑥) ∈ (dom (𝐺 ∖ I ) ∖ {𝑥}))) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
39 | 18, 28, 31, 38 | syl12anc 1324 |
. . . 4
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ dom (𝐺 ∖ I )) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
40 | 39 | adantlr 751 |
. . 3
⊢
(((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) ∧ 𝑥 ∈ dom (𝐺 ∖ I )) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
41 | | simplrr 801 |
. . . . . . . 8
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → dom (𝐺 ∖ I ) = dom (𝐹 ∖ I )) |
42 | 41 | eleq2d 2687 |
. . . . . . 7
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐺 ∖ I ) ↔ 𝑥 ∈ dom (𝐹 ∖ I ))) |
43 | | fnelnfp 6443 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
44 | 2, 43 | sylan 488 |
. . . . . . 7
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐹 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
45 | 42, 44 | bitrd 268 |
. . . . . 6
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐺 ∖ I ) ↔ (𝐹‘𝑥) ≠ 𝑥)) |
46 | 45 | necon2bbid 2837 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑥 ↔ ¬ 𝑥 ∈ dom (𝐺 ∖ I ))) |
47 | 46 | biimpar 502 |
. . . 4
⊢
(((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ dom (𝐺 ∖ I )) → (𝐹‘𝑥) = 𝑥) |
48 | | fnelnfp 6443 |
. . . . . . 7
⊢ ((𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐺 ∖ I ) ↔ (𝐺‘𝑥) ≠ 𝑥)) |
49 | 4, 48 | sylan 488 |
. . . . . 6
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → (𝑥 ∈ dom (𝐺 ∖ I ) ↔ (𝐺‘𝑥) ≠ 𝑥)) |
50 | 49 | necon2bbid 2837 |
. . . . 5
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → ((𝐺‘𝑥) = 𝑥 ↔ ¬ 𝑥 ∈ dom (𝐺 ∖ I ))) |
51 | 50 | biimpar 502 |
. . . 4
⊢
(((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ dom (𝐺 ∖ I )) → (𝐺‘𝑥) = 𝑥) |
52 | 47, 51 | eqtr4d 2659 |
. . 3
⊢
(((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) ∧ ¬ 𝑥 ∈ dom (𝐺 ∖ I )) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
53 | 40, 52 | pm2.61dan 832 |
. 2
⊢ ((((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) ∧
𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
54 | 2, 4, 53 | eqfnfvd 6314 |
1
⊢ (((𝐹:𝐴–1-1-onto→𝐴 ∧ 𝐺:𝐴–1-1-onto→𝐴) ∧ (dom (𝐹 ∖ I ) ≈ 2𝑜
∧ dom (𝐺 ∖ I ) =
dom (𝐹 ∖ I ))) →
𝐹 = 𝐺) |