Step |
Hyp |
Ref |
Expression |
1 |
|
reeanv |
⊢ ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ↔ ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) |
2 |
|
breq2 |
⊢ ( 𝑣 = 𝑝 → ( 𝑢 <s 𝑣 ↔ 𝑢 <s 𝑝 ) ) |
3 |
2
|
notbid |
⊢ ( 𝑣 = 𝑝 → ( ¬ 𝑢 <s 𝑣 ↔ ¬ 𝑢 <s 𝑝 ) ) |
4 |
|
reseq1 |
⊢ ( 𝑣 = 𝑝 → ( 𝑣 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) |
5 |
4
|
eqeq2d |
⊢ ( 𝑣 = 𝑝 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) ) |
6 |
3 5
|
imbi12d |
⊢ ( 𝑣 = 𝑝 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑢 <s 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) ) ) |
7 |
|
simprl2 |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) |
8 |
7
|
adantl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) |
9 |
|
simprlr |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝑝 ∈ 𝐴 ) |
10 |
6 8 9
|
rspcdva |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑢 <s 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) ) |
11 |
|
breq2 |
⊢ ( 𝑣 = 𝑢 → ( 𝑝 <s 𝑣 ↔ 𝑝 <s 𝑢 ) ) |
12 |
11
|
notbid |
⊢ ( 𝑣 = 𝑢 → ( ¬ 𝑝 <s 𝑣 ↔ ¬ 𝑝 <s 𝑢 ) ) |
13 |
|
reseq1 |
⊢ ( 𝑣 = 𝑢 → ( 𝑣 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) |
14 |
13
|
eqeq2d |
⊢ ( 𝑣 = 𝑢 → ( ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) ) |
15 |
12 14
|
imbi12d |
⊢ ( 𝑣 = 𝑢 → ( ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑝 <s 𝑢 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) ) ) |
16 |
|
simprr2 |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) |
17 |
16
|
adantl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) |
18 |
|
simprll |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝑢 ∈ 𝐴 ) |
19 |
15 17 18
|
rspcdva |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑝 <s 𝑢 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ) ) |
20 |
|
eqcom |
⊢ ( ( 𝑝 ↾ suc 𝐺 ) = ( 𝑢 ↾ suc 𝐺 ) ↔ ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) |
21 |
19 20
|
syl6ib |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑝 <s 𝑢 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) ) |
22 |
|
simpl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝐴 ⊆ No ) |
23 |
22 18
|
sseldd |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝑢 ∈ No ) |
24 |
22 9
|
sseldd |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝑝 ∈ No ) |
25 |
|
sltso |
⊢ <s Or No |
26 |
|
soasym |
⊢ ( ( <s Or No ∧ ( 𝑢 ∈ No ∧ 𝑝 ∈ No ) ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) ) |
27 |
25 26
|
mpan |
⊢ ( ( 𝑢 ∈ No ∧ 𝑝 ∈ No ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) ) |
28 |
23 24 27
|
syl2anc |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) ) |
29 |
|
imor |
⊢ ( ( 𝑢 <s 𝑝 → ¬ 𝑝 <s 𝑢 ) ↔ ( ¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢 ) ) |
30 |
28 29
|
sylib |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ¬ 𝑢 <s 𝑝 ∨ ¬ 𝑝 <s 𝑢 ) ) |
31 |
10 21 30
|
mpjaod |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) |
32 |
31
|
fveq1d |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑢 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( ( 𝑝 ↾ suc 𝐺 ) ‘ 𝐺 ) ) |
33 |
|
simprl1 |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) → 𝐺 ∈ dom 𝑢 ) |
34 |
33
|
adantl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝐺 ∈ dom 𝑢 ) |
35 |
|
sucidg |
⊢ ( 𝐺 ∈ dom 𝑢 → 𝐺 ∈ suc 𝐺 ) |
36 |
34 35
|
syl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝐺 ∈ suc 𝐺 ) |
37 |
36
|
fvresd |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑢 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( 𝑢 ‘ 𝐺 ) ) |
38 |
36
|
fvresd |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( ( 𝑝 ↾ suc 𝐺 ) ‘ 𝐺 ) = ( 𝑝 ‘ 𝐺 ) ) |
39 |
32 37 38
|
3eqtr3d |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 ‘ 𝐺 ) = ( 𝑝 ‘ 𝐺 ) ) |
40 |
|
simprl3 |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) → ( 𝑢 ‘ 𝐺 ) = 𝑥 ) |
41 |
40
|
adantl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( 𝑢 ‘ 𝐺 ) = 𝑥 ) |
42 |
|
simprr3 |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) → ( 𝑝 ‘ 𝐺 ) = 𝑦 ) |
43 |
42
|
adantl |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → ( 𝑝 ‘ 𝐺 ) = 𝑦 ) |
44 |
39 41 43
|
3eqtr3d |
⊢ ( ( 𝐴 ⊆ No ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ∧ ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) ) → 𝑥 = 𝑦 ) |
45 |
44
|
expr |
⊢ ( ( 𝐴 ⊆ No ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑝 ∈ 𝐴 ) ) → ( ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) ) |
46 |
45
|
rexlimdvva |
⊢ ( 𝐴 ⊆ No → ( ∃ 𝑢 ∈ 𝐴 ∃ 𝑝 ∈ 𝐴 ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) ) |
47 |
1 46
|
syl5bir |
⊢ ( 𝐴 ⊆ No → ( ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) ) |
48 |
47
|
alrimivv |
⊢ ( 𝐴 ⊆ No → ∀ 𝑥 ∀ 𝑦 ( ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) ) |
49 |
|
eqeq2 |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑢 ‘ 𝐺 ) = 𝑥 ↔ ( 𝑢 ‘ 𝐺 ) = 𝑦 ) ) |
50 |
49
|
3anbi3d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑦 ) ) ) |
51 |
50
|
rexbidv |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑦 ) ) ) |
52 |
|
dmeq |
⊢ ( 𝑢 = 𝑝 → dom 𝑢 = dom 𝑝 ) |
53 |
52
|
eleq2d |
⊢ ( 𝑢 = 𝑝 → ( 𝐺 ∈ dom 𝑢 ↔ 𝐺 ∈ dom 𝑝 ) ) |
54 |
|
breq1 |
⊢ ( 𝑢 = 𝑝 → ( 𝑢 <s 𝑣 ↔ 𝑝 <s 𝑣 ) ) |
55 |
54
|
notbid |
⊢ ( 𝑢 = 𝑝 → ( ¬ 𝑢 <s 𝑣 ↔ ¬ 𝑝 <s 𝑣 ) ) |
56 |
|
reseq1 |
⊢ ( 𝑢 = 𝑝 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑝 ↾ suc 𝐺 ) ) |
57 |
56
|
eqeq1d |
⊢ ( 𝑢 = 𝑝 → ( ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ↔ ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) |
58 |
55 57
|
imbi12d |
⊢ ( 𝑢 = 𝑝 → ( ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) |
59 |
58
|
ralbidv |
⊢ ( 𝑢 = 𝑝 → ( ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ↔ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ) ) |
60 |
|
fveq1 |
⊢ ( 𝑢 = 𝑝 → ( 𝑢 ‘ 𝐺 ) = ( 𝑝 ‘ 𝐺 ) ) |
61 |
60
|
eqeq1d |
⊢ ( 𝑢 = 𝑝 → ( ( 𝑢 ‘ 𝐺 ) = 𝑦 ↔ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) |
62 |
53 59 61
|
3anbi123d |
⊢ ( 𝑢 = 𝑝 → ( ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑦 ) ↔ ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) |
63 |
62
|
cbvrexvw |
⊢ ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑦 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) |
64 |
51 63
|
bitrdi |
⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) ) |
65 |
64
|
mo4 |
⊢ ( ∃* 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ↔ ∀ 𝑥 ∀ 𝑦 ( ( ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ∧ ∃ 𝑝 ∈ 𝐴 ( 𝐺 ∈ dom 𝑝 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑝 <s 𝑣 → ( 𝑝 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑝 ‘ 𝐺 ) = 𝑦 ) ) → 𝑥 = 𝑦 ) ) |
66 |
48 65
|
sylibr |
⊢ ( 𝐴 ⊆ No → ∃* 𝑥 ∃ 𝑢 ∈ 𝐴 ( 𝐺 ∈ dom 𝑢 ∧ ∀ 𝑣 ∈ 𝐴 ( ¬ 𝑢 <s 𝑣 → ( 𝑢 ↾ suc 𝐺 ) = ( 𝑣 ↾ suc 𝐺 ) ) ∧ ( 𝑢 ‘ 𝐺 ) = 𝑥 ) ) |