Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . 3
⊢ A = {f ∣
∃x ∈ On (f Fn
x ∧ ∀y ∈ x (f‘y) =
(𝐹‘(f ↾ y)))} |
2 | | vex 2554 |
. . 3
⊢ g ∈
V |
3 | 1, 2 | tfrlem3a 5866 |
. 2
⊢ (g ∈ A ↔ ∃z ∈ On (g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎)))) |
4 | | vex 2554 |
. . 3
⊢ ℎ ∈
V |
5 | 1, 4 | tfrlem3a 5866 |
. 2
⊢ (ℎ ∈
A ↔ ∃w ∈ On (ℎ Fn w
∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) |
6 | | reeanv 2473 |
. . 3
⊢ (∃z ∈ On ∃w ∈ On ((g Fn z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃z ∈ On (g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ ∃w ∈ On (ℎ Fn w
∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))) |
7 | | simp2ll 970 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → g Fn
z) |
8 | | simp3l 931 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → xgu) |
9 | | fnbr 4944 |
. . . . . . . . . 10
⊢
((g Fn z ∧ xgu) → x
∈ z) |
10 | 7, 8, 9 | syl2anc 391 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → x
∈ z) |
11 | | simp2rl 972 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ℎ Fn w) |
12 | | simp3r 932 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → xℎv) |
13 | | fnbr 4944 |
. . . . . . . . . 10
⊢ ((ℎ Fn w ∧ xℎv) →
x ∈
w) |
14 | 11, 12, 13 | syl2anc 391 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → x
∈ w) |
15 | | elin 3120 |
. . . . . . . . 9
⊢ (x ∈ (z ∩ w)
↔ (x ∈ z ∧ x ∈ w)) |
16 | 10, 14, 15 | sylanbrc 394 |
. . . . . . . 8
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → x
∈ (z
∩ w)) |
17 | | onin 4089 |
. . . . . . . . . 10
⊢
((z ∈ On ∧ w ∈ On) →
(z ∩ w) ∈
On) |
18 | 17 | 3ad2ant1 924 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (z
∩ w) ∈ On) |
19 | | fnfun 4939 |
. . . . . . . . . . 11
⊢ (g Fn z →
Fun g) |
20 | 7, 19 | syl 14 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → Fun g) |
21 | | inss1 3151 |
. . . . . . . . . . 11
⊢ (z ∩ w)
⊆ z |
22 | | fndm 4941 |
. . . . . . . . . . . 12
⊢ (g Fn z →
dom g = z) |
23 | 7, 22 | syl 14 |
. . . . . . . . . . 11
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → dom g
= z) |
24 | 21, 23 | syl5sseqr 2988 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (z
∩ w) ⊆ dom g) |
25 | 20, 24 | jca 290 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (Fun g ∧ (z ∩ w)
⊆ dom g)) |
26 | | fnfun 4939 |
. . . . . . . . . . 11
⊢ (ℎ Fn w → Fun ℎ) |
27 | 11, 26 | syl 14 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → Fun ℎ) |
28 | | inss2 3152 |
. . . . . . . . . . 11
⊢ (z ∩ w)
⊆ w |
29 | | fndm 4941 |
. . . . . . . . . . . 12
⊢ (ℎ Fn w → dom ℎ = w) |
30 | 11, 29 | syl 14 |
. . . . . . . . . . 11
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → dom ℎ = w) |
31 | 28, 30 | syl5sseqr 2988 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (z
∩ w) ⊆ dom ℎ) |
32 | 27, 31 | jca 290 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (Fun ℎ ∧ (z ∩ w)
⊆ dom ℎ)) |
33 | | simp2lr 971 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) |
34 | | ssralv 2998 |
. . . . . . . . . 10
⊢
((z ∩ w) ⊆ z
→ (∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎)) → ∀𝑎 ∈
(z ∩ w)(g‘𝑎) = (𝐹‘(g ↾ 𝑎)))) |
35 | 21, 33, 34 | mpsyl 59 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ∀𝑎 ∈
(z ∩ w)(g‘𝑎) = (𝐹‘(g ↾ 𝑎))) |
36 | | simp2rr 973 |
. . . . . . . . . 10
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))) |
37 | | ssralv 2998 |
. . . . . . . . . 10
⊢
((z ∩ w) ⊆ w
→ (∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈
(z ∩ w)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) |
38 | 28, 36, 37 | mpsyl 59 |
. . . . . . . . 9
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ∀𝑎 ∈
(z ∩ w)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))) |
39 | 18, 25, 32, 35, 38 | tfrlem1 5864 |
. . . . . . . 8
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → ∀𝑎 ∈
(z ∩ w)(g‘𝑎) = (ℎ‘𝑎)) |
40 | | fveq2 5121 |
. . . . . . . . . 10
⊢ (𝑎 = x → (g‘𝑎) = (g‘x)) |
41 | | fveq2 5121 |
. . . . . . . . . 10
⊢ (𝑎 = x → (ℎ‘𝑎) = (ℎ‘x)) |
42 | 40, 41 | eqeq12d 2051 |
. . . . . . . . 9
⊢ (𝑎 = x → ((g‘𝑎) = (ℎ‘𝑎) ↔ (g‘x) =
(ℎ‘x))) |
43 | 42 | rspcv 2646 |
. . . . . . . 8
⊢ (x ∈ (z ∩ w)
→ (∀𝑎 ∈
(z ∩ w)(g‘𝑎) = (ℎ‘𝑎) → (g‘x) =
(ℎ‘x))) |
44 | 16, 39, 43 | sylc 56 |
. . . . . . 7
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (g‘x) =
(ℎ‘x)) |
45 | | funbrfv 5155 |
. . . . . . . 8
⊢ (Fun
g → (xgu → (g‘x) =
u)) |
46 | 20, 8, 45 | sylc 56 |
. . . . . . 7
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (g‘x) =
u) |
47 | | funbrfv 5155 |
. . . . . . . 8
⊢ (Fun
ℎ → (xℎv →
(ℎ‘x) = v)) |
48 | 27, 12, 47 | sylc 56 |
. . . . . . 7
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → (ℎ‘x)
= v) |
49 | 44, 46, 48 | 3eqtr3d 2077 |
. . . . . 6
⊢
(((z ∈ On ∧ w ∈ On) ∧ ((g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧
(xgu ∧ xℎv)) → u =
v) |
50 | 49 | 3exp 1102 |
. . . . 5
⊢
((z ∈ On ∧ w ∈ On) →
(((g Fn z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((xgu ∧ xℎv) →
u = v))) |
51 | 50 | rexlimdva 2427 |
. . . 4
⊢ (z ∈ On →
(∃w
∈ On ((g
Fn z ∧
∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((xgu ∧ xℎv) →
u = v))) |
52 | 51 | rexlimiv 2421 |
. . 3
⊢ (∃z ∈ On ∃w ∈ On ((g Fn z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ (ℎ Fn w ∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((xgu ∧ xℎv) →
u = v)) |
53 | 6, 52 | sylbir 125 |
. 2
⊢ ((∃z ∈ On (g Fn
z ∧ ∀𝑎 ∈ z (g‘𝑎) = (𝐹‘(g ↾ 𝑎))) ∧ ∃w ∈ On (ℎ Fn w
∧ ∀𝑎 ∈ w (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((xgu ∧ xℎv) →
u = v)) |
54 | 3, 5, 53 | syl2anb 275 |
1
⊢
((g ∈ A ∧ ℎ
∈ A)
→ ((xgu ∧ xℎv) → u =
v)) |