Step |
Hyp |
Ref |
Expression |
1 |
|
f1ofn |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → 𝐹 Fn 𝐴 ) |
2 |
1
|
ad2antrr |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 Fn 𝐴 ) |
3 |
|
f1ofn |
⊢ ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 → 𝐺 Fn 𝐴 ) |
4 |
3
|
ad2antlr |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐺 Fn 𝐴 ) |
5 |
|
1onn |
⊢ 1o ∈ ω |
6 |
|
simplrr |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) |
7 |
|
simplrl |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐹 ∖ I ) ≈ 2o ) |
8 |
|
df-2o |
⊢ 2o = suc 1o |
9 |
7 8
|
breqtrdi |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐹 ∖ I ) ≈ suc 1o ) |
10 |
6 9
|
eqbrtrd |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → dom ( 𝐺 ∖ I ) ≈ suc 1o ) |
11 |
|
simpr |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → 𝑥 ∈ dom ( 𝐺 ∖ I ) ) |
12 |
|
dif1en |
⊢ ( ( 1o ∈ ω ∧ dom ( 𝐺 ∖ I ) ≈ suc 1o ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o ) |
13 |
5 10 11 12
|
mp3an2i |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o ) |
14 |
|
euen1b |
⊢ ( ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o ↔ ∃! 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
15 |
|
eumo |
⊢ ( ∃! 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
16 |
14 15
|
sylbi |
⊢ ( ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ≈ 1o → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
17 |
13 16
|
syl |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
18 |
|
f1omvdmvd |
⊢ ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) |
19 |
18
|
ex |
⊢ ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) → ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) ) |
20 |
19
|
ad2antrr |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) → ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) ) |
21 |
|
eleq2 |
⊢ ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) ) |
22 |
21
|
ad2antll |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) ) |
23 |
|
difeq1 |
⊢ ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) = ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) |
24 |
23
|
eleq2d |
⊢ ( dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) ) |
25 |
24
|
ad2antll |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐹 ∖ I ) ∖ { 𝑥 } ) ) ) |
26 |
20 22 25
|
3imtr4d |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) → ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) |
27 |
26
|
imp |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
28 |
|
f1omvdmvd |
⊢ ( ( 𝐺 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
29 |
28
|
ad4ant24 |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) |
30 |
|
fvex |
⊢ ( 𝐹 ‘ 𝑥 ) ∈ V |
31 |
|
fvex |
⊢ ( 𝐺 ‘ 𝑥 ) ∈ V |
32 |
30 31
|
pm3.2i |
⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐺 ‘ 𝑥 ) ∈ V ) |
33 |
|
eleq1 |
⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) |
34 |
|
eleq1 |
⊢ ( 𝑦 = ( 𝐺 ‘ 𝑥 ) → ( 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) |
35 |
33 34
|
moi |
⊢ ( ( ( ( 𝐹 ‘ 𝑥 ) ∈ V ∧ ( 𝐺 ‘ 𝑥 ) ∈ V ) ∧ ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
36 |
32 35
|
mp3an1 |
⊢ ( ( ∃* 𝑦 𝑦 ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( ( 𝐹 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ∧ ( 𝐺 ‘ 𝑥 ) ∈ ( dom ( 𝐺 ∖ I ) ∖ { 𝑥 } ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
37 |
17 27 29 36
|
syl12anc |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
38 |
37
|
adantlr |
⊢ ( ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
39 |
|
simplrr |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) |
40 |
39
|
eleq2d |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ 𝑥 ∈ dom ( 𝐹 ∖ I ) ) ) |
41 |
|
fnelnfp |
⊢ ( ( 𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) ) |
42 |
2 41
|
sylan |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐹 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) ) |
43 |
40 42
|
bitrd |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐹 ‘ 𝑥 ) ≠ 𝑥 ) ) |
44 |
43
|
necon2bbid |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 𝑥 ↔ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) ) |
45 |
44
|
biimpar |
⊢ ( ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = 𝑥 ) |
46 |
|
fnelnfp |
⊢ ( ( 𝐺 Fn 𝐴 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐺 ‘ 𝑥 ) ≠ 𝑥 ) ) |
47 |
4 46
|
sylan |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 ∈ dom ( 𝐺 ∖ I ) ↔ ( 𝐺 ‘ 𝑥 ) ≠ 𝑥 ) ) |
48 |
47
|
necon2bbid |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) = 𝑥 ↔ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) ) |
49 |
48
|
biimpar |
⊢ ( ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐺 ‘ 𝑥 ) = 𝑥 ) |
50 |
45 49
|
eqtr4d |
⊢ ( ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ¬ 𝑥 ∈ dom ( 𝐺 ∖ I ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
51 |
38 50
|
pm2.61dan |
⊢ ( ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑥 ) ) |
52 |
2 4 51
|
eqfnfvd |
⊢ ( ( ( 𝐹 : 𝐴 –1-1-onto→ 𝐴 ∧ 𝐺 : 𝐴 –1-1-onto→ 𝐴 ) ∧ ( dom ( 𝐹 ∖ I ) ≈ 2o ∧ dom ( 𝐺 ∖ I ) = dom ( 𝐹 ∖ I ) ) ) → 𝐹 = 𝐺 ) |