Step | Hyp | Ref
| Expression |
1 | | tfrlem.1 |
. . 3
⊢ 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑓‘𝑦) = (𝐹‘(𝑓 ↾ 𝑦)))} |
2 | | vex 2560 |
. . 3
⊢ 𝑔 ∈ V |
3 | 1, 2 | tfrlem3a 5925 |
. 2
⊢ (𝑔 ∈ 𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) |
4 | | vex 2560 |
. . 3
⊢ ℎ ∈ V |
5 | 1, 4 | tfrlem3a 5925 |
. 2
⊢ (ℎ ∈ 𝐴 ↔ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) |
6 | | reeanv 2479 |
. . 3
⊢
(∃𝑧 ∈ On
∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))))) |
7 | | simp2ll 971 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑔 Fn 𝑧) |
8 | | simp3l 932 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥𝑔𝑢) |
9 | | fnbr 5001 |
. . . . . . . . . 10
⊢ ((𝑔 Fn 𝑧 ∧ 𝑥𝑔𝑢) → 𝑥 ∈ 𝑧) |
10 | 7, 8, 9 | syl2anc 391 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑧) |
11 | | simp2rl 973 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ℎ Fn 𝑤) |
12 | | simp3r 933 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥ℎ𝑣) |
13 | | fnbr 5001 |
. . . . . . . . . 10
⊢ ((ℎ Fn 𝑤 ∧ 𝑥ℎ𝑣) → 𝑥 ∈ 𝑤) |
14 | 11, 12, 13 | syl2anc 391 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ 𝑤) |
15 | | elin 3126 |
. . . . . . . . 9
⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) ↔ (𝑥 ∈ 𝑧 ∧ 𝑥 ∈ 𝑤)) |
16 | 10, 14, 15 | sylanbrc 394 |
. . . . . . . 8
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑥 ∈ (𝑧 ∩ 𝑤)) |
17 | | onin 4123 |
. . . . . . . . . 10
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧 ∩ 𝑤) ∈ On) |
18 | 17 | 3ad2ant1 925 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ∈ On) |
19 | | fnfun 4996 |
. . . . . . . . . . 11
⊢ (𝑔 Fn 𝑧 → Fun 𝑔) |
20 | 7, 19 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun 𝑔) |
21 | | inss1 3157 |
. . . . . . . . . . 11
⊢ (𝑧 ∩ 𝑤) ⊆ 𝑧 |
22 | | fndm 4998 |
. . . . . . . . . . . 12
⊢ (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧) |
23 | 7, 22 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom 𝑔 = 𝑧) |
24 | 21, 23 | syl5sseqr 2994 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom 𝑔) |
25 | 20, 24 | jca 290 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun 𝑔 ∧ (𝑧 ∩ 𝑤) ⊆ dom 𝑔)) |
26 | | fnfun 4996 |
. . . . . . . . . . 11
⊢ (ℎ Fn 𝑤 → Fun ℎ) |
27 | 11, 26 | syl 14 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → Fun ℎ) |
28 | | inss2 3158 |
. . . . . . . . . . 11
⊢ (𝑧 ∩ 𝑤) ⊆ 𝑤 |
29 | | fndm 4998 |
. . . . . . . . . . . 12
⊢ (ℎ Fn 𝑤 → dom ℎ = 𝑤) |
30 | 11, 29 | syl 14 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → dom ℎ = 𝑤) |
31 | 28, 30 | syl5sseqr 2994 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑧 ∩ 𝑤) ⊆ dom ℎ) |
32 | 27, 31 | jca 290 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (Fun ℎ ∧ (𝑧 ∩ 𝑤) ⊆ dom ℎ)) |
33 | | simp2lr 972 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) |
34 | | ssralv 3004 |
. . . . . . . . . 10
⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑧 → (∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎)))) |
35 | 21, 33, 34 | mpsyl 59 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) |
36 | | simp2rr 974 |
. . . . . . . . . 10
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))) |
37 | | ssralv 3004 |
. . . . . . . . . 10
⊢ ((𝑧 ∩ 𝑤) ⊆ 𝑤 → (∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) |
38 | 28, 36, 37 | mpsyl 59 |
. . . . . . . . 9
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎))) |
39 | 18, 25, 32, 35, 38 | tfrlem1 5923 |
. . . . . . . 8
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → ∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎)) |
40 | | fveq2 5178 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (𝑔‘𝑎) = (𝑔‘𝑥)) |
41 | | fveq2 5178 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑥 → (ℎ‘𝑎) = (ℎ‘𝑥)) |
42 | 40, 41 | eqeq12d 2054 |
. . . . . . . . 9
⊢ (𝑎 = 𝑥 → ((𝑔‘𝑎) = (ℎ‘𝑎) ↔ (𝑔‘𝑥) = (ℎ‘𝑥))) |
43 | 42 | rspcv 2652 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑧 ∩ 𝑤) → (∀𝑎 ∈ (𝑧 ∩ 𝑤)(𝑔‘𝑎) = (ℎ‘𝑎) → (𝑔‘𝑥) = (ℎ‘𝑥))) |
44 | 16, 39, 43 | sylc 56 |
. . . . . . 7
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = (ℎ‘𝑥)) |
45 | | funbrfv 5212 |
. . . . . . . 8
⊢ (Fun
𝑔 → (𝑥𝑔𝑢 → (𝑔‘𝑥) = 𝑢)) |
46 | 20, 8, 45 | sylc 56 |
. . . . . . 7
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (𝑔‘𝑥) = 𝑢) |
47 | | funbrfv 5212 |
. . . . . . . 8
⊢ (Fun
ℎ → (𝑥ℎ𝑣 → (ℎ‘𝑥) = 𝑣)) |
48 | 27, 12, 47 | sylc 56 |
. . . . . . 7
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → (ℎ‘𝑥) = 𝑣) |
49 | 44, 46, 48 | 3eqtr3d 2080 |
. . . . . 6
⊢ (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) ∧ (𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣)) → 𝑢 = 𝑣) |
50 | 49 | 3exp 1103 |
. . . . 5
⊢ ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))) |
51 | 50 | rexlimdva 2433 |
. . . 4
⊢ (𝑧 ∈ On → (∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣))) |
52 | 51 | rexlimiv 2427 |
. . 3
⊢
(∃𝑧 ∈ On
∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |
53 | 6, 52 | sylbir 125 |
. 2
⊢
((∃𝑧 ∈ On
(𝑔 Fn 𝑧 ∧ ∀𝑎 ∈ 𝑧 (𝑔‘𝑎) = (𝐹‘(𝑔 ↾ 𝑎))) ∧ ∃𝑤 ∈ On (ℎ Fn 𝑤 ∧ ∀𝑎 ∈ 𝑤 (ℎ‘𝑎) = (𝐹‘(ℎ ↾ 𝑎)))) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |
54 | 3, 5, 53 | syl2anb 275 |
1
⊢ ((𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴) → ((𝑥𝑔𝑢 ∧ 𝑥ℎ𝑣) → 𝑢 = 𝑣)) |