Step |
Hyp |
Ref |
Expression |
1 |
|
tfrlem.1 |
⊢ 𝐴 = { 𝑓 ∣ ∃ 𝑥 ∈ On ( 𝑓 Fn 𝑥 ∧ ∀ 𝑦 ∈ 𝑥 ( 𝑓 ‘ 𝑦 ) = ( 𝐹 ‘ ( 𝑓 ↾ 𝑦 ) ) ) } |
2 |
|
vex |
⊢ 𝑔 ∈ V |
3 |
1 2
|
tfrlem3a |
⊢ ( 𝑔 ∈ 𝐴 ↔ ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ) |
4 |
|
vex |
⊢ ℎ ∈ V |
5 |
1 4
|
tfrlem3a |
⊢ ( ℎ ∈ 𝐴 ↔ ∃ 𝑤 ∈ On ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) |
6 |
|
reeanv |
⊢ ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ↔ ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ∃ 𝑤 ∈ On ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑎 = 𝑥 → ( 𝑔 ‘ 𝑎 ) = ( 𝑔 ‘ 𝑥 ) ) |
8 |
|
fveq2 |
⊢ ( 𝑎 = 𝑥 → ( ℎ ‘ 𝑎 ) = ( ℎ ‘ 𝑥 ) ) |
9 |
7 8
|
eqeq12d |
⊢ ( 𝑎 = 𝑥 → ( ( 𝑔 ‘ 𝑎 ) = ( ℎ ‘ 𝑎 ) ↔ ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) ) |
10 |
|
onin |
⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( 𝑧 ∩ 𝑤 ) ∈ On ) |
11 |
10
|
3ad2ant1 |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑧 ∩ 𝑤 ) ∈ On ) |
12 |
|
simp2ll |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑔 Fn 𝑧 ) |
13 |
|
fnfun |
⊢ ( 𝑔 Fn 𝑧 → Fun 𝑔 ) |
14 |
12 13
|
syl |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → Fun 𝑔 ) |
15 |
|
inss1 |
⊢ ( 𝑧 ∩ 𝑤 ) ⊆ 𝑧 |
16 |
12
|
fndmd |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → dom 𝑔 = 𝑧 ) |
17 |
15 16
|
sseqtrrid |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑧 ∩ 𝑤 ) ⊆ dom 𝑔 ) |
18 |
14 17
|
jca |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( Fun 𝑔 ∧ ( 𝑧 ∩ 𝑤 ) ⊆ dom 𝑔 ) ) |
19 |
|
simp2rl |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ℎ Fn 𝑤 ) |
20 |
|
fnfun |
⊢ ( ℎ Fn 𝑤 → Fun ℎ ) |
21 |
19 20
|
syl |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → Fun ℎ ) |
22 |
|
inss2 |
⊢ ( 𝑧 ∩ 𝑤 ) ⊆ 𝑤 |
23 |
19
|
fndmd |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → dom ℎ = 𝑤 ) |
24 |
22 23
|
sseqtrrid |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑧 ∩ 𝑤 ) ⊆ dom ℎ ) |
25 |
21 24
|
jca |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( Fun ℎ ∧ ( 𝑧 ∩ 𝑤 ) ⊆ dom ℎ ) ) |
26 |
|
simp2lr |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) |
27 |
|
ssralv |
⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ 𝑧 → ( ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ) |
28 |
15 26 27
|
mpsyl |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) |
29 |
|
simp2rr |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) |
30 |
|
ssralv |
⊢ ( ( 𝑧 ∩ 𝑤 ) ⊆ 𝑤 → ( ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) |
31 |
22 29 30
|
mpsyl |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) |
32 |
11 18 25 28 31
|
tfrlem1 |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ∀ 𝑎 ∈ ( 𝑧 ∩ 𝑤 ) ( 𝑔 ‘ 𝑎 ) = ( ℎ ‘ 𝑎 ) ) |
33 |
|
simp3l |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 𝑔 𝑢 ) |
34 |
|
fnbr |
⊢ ( ( 𝑔 Fn 𝑧 ∧ 𝑥 𝑔 𝑢 ) → 𝑥 ∈ 𝑧 ) |
35 |
12 33 34
|
syl2anc |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ 𝑧 ) |
36 |
|
simp3r |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ℎ 𝑣 ) |
37 |
|
fnbr |
⊢ ( ( ℎ Fn 𝑤 ∧ 𝑥 ℎ 𝑣 ) → 𝑥 ∈ 𝑤 ) |
38 |
19 36 37
|
syl2anc |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ 𝑤 ) |
39 |
35 38
|
elind |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑥 ∈ ( 𝑧 ∩ 𝑤 ) ) |
40 |
9 32 39
|
rspcdva |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑔 ‘ 𝑥 ) = ( ℎ ‘ 𝑥 ) ) |
41 |
|
funbrfv |
⊢ ( Fun 𝑔 → ( 𝑥 𝑔 𝑢 → ( 𝑔 ‘ 𝑥 ) = 𝑢 ) ) |
42 |
14 33 41
|
sylc |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( 𝑔 ‘ 𝑥 ) = 𝑢 ) |
43 |
|
funbrfv |
⊢ ( Fun ℎ → ( 𝑥 ℎ 𝑣 → ( ℎ ‘ 𝑥 ) = 𝑣 ) ) |
44 |
21 36 43
|
sylc |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → ( ℎ ‘ 𝑥 ) = 𝑣 ) |
45 |
40 42 44
|
3eqtr3d |
⊢ ( ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) ∧ ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) ∧ ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) ) → 𝑢 = 𝑣 ) |
46 |
45
|
3exp |
⊢ ( ( 𝑧 ∈ On ∧ 𝑤 ∈ On ) → ( ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) ) |
47 |
46
|
rexlimivv |
⊢ ( ∃ 𝑧 ∈ On ∃ 𝑤 ∈ On ( ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) |
48 |
6 47
|
sylbir |
⊢ ( ( ∃ 𝑧 ∈ On ( 𝑔 Fn 𝑧 ∧ ∀ 𝑎 ∈ 𝑧 ( 𝑔 ‘ 𝑎 ) = ( 𝐹 ‘ ( 𝑔 ↾ 𝑎 ) ) ) ∧ ∃ 𝑤 ∈ On ( ℎ Fn 𝑤 ∧ ∀ 𝑎 ∈ 𝑤 ( ℎ ‘ 𝑎 ) = ( 𝐹 ‘ ( ℎ ↾ 𝑎 ) ) ) ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) |
49 |
3 5 48
|
syl2anb |
⊢ ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( ( 𝑥 𝑔 𝑢 ∧ 𝑥 ℎ 𝑣 ) → 𝑢 = 𝑣 ) ) |