Step | Hyp | Ref
| Expression |
1 | | ssid 2958 |
. 2
⊢ A ⊆ A |
2 | | tfrlem1.1 |
. . 3
⊢ (φ → A ∈
On) |
3 | | sseq1 2960 |
. . . . . 6
⊢ (y = A →
(y ⊆ A ↔ A
⊆ A)) |
4 | | raleq 2499 |
. . . . . 6
⊢ (y = A →
(∀x
∈ y
(𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ A (𝐹‘x) = (𝐺‘x))) |
5 | 3, 4 | imbi12d 223 |
. . . . 5
⊢ (y = A →
((y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)) ↔ (A
⊆ A → ∀x ∈ A (𝐹‘x) = (𝐺‘x)))) |
6 | 5 | imbi2d 219 |
. . . 4
⊢ (y = A →
((φ → (y ⊆ A
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x))) ↔ (φ → (A ⊆ A
→ ∀x ∈ A (𝐹‘x) = (𝐺‘x))))) |
7 | | sseq1 2960 |
. . . . . . 7
⊢ (y = z →
(y ⊆ A ↔ z
⊆ A)) |
8 | | raleq 2499 |
. . . . . . 7
⊢ (y = z →
(∀x
∈ y
(𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) |
9 | 7, 8 | imbi12d 223 |
. . . . . 6
⊢ (y = z →
((y ⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)) ↔ (z
⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)))) |
10 | 9 | imbi2d 219 |
. . . . 5
⊢ (y = z →
((φ → (y ⊆ A
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x))) ↔ (φ → (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))))) |
11 | | r19.21v 2390 |
. . . . . 6
⊢ (∀z ∈ y (φ → (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ↔ (φ → ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x)))) |
12 | | simplll 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ φ) |
13 | 12 | adantr 261 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
φ) |
14 | | tfrlem1.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (φ → (Fun 𝐹 ∧ A ⊆ dom 𝐹)) |
15 | 13, 14 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(Fun 𝐹 ∧ A ⊆ dom
𝐹)) |
16 | 15 | simpld 105 |
. . . . . . . . . . . . . . . 16
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) → Fun
𝐹) |
17 | | funfn 4874 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
18 | 16, 17 | sylib 127 |
. . . . . . . . . . . . . . 15
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
𝐹 Fn dom 𝐹) |
19 | | simpllr 486 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ y ∈ On) |
20 | | eloni 4078 |
. . . . . . . . . . . . . . . . . . 19
⊢ (y ∈ On → Ord
y) |
21 | 19, 20 | syl 14 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ Ord y) |
22 | | ordelss 4082 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Ord
y ∧
w ∈
y) → w ⊆ y) |
23 | 21, 22 | sylan 267 |
. . . . . . . . . . . . . . . . 17
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
w ⊆ y) |
24 | | simplr 482 |
. . . . . . . . . . . . . . . . 17
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
y ⊆ A) |
25 | 23, 24 | sstrd 2949 |
. . . . . . . . . . . . . . . 16
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
w ⊆ A) |
26 | 15 | simprd 107 |
. . . . . . . . . . . . . . . 16
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
A ⊆ dom 𝐹) |
27 | 25, 26 | sstrd 2949 |
. . . . . . . . . . . . . . 15
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
w ⊆ dom 𝐹) |
28 | | fnssres 4955 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 Fn dom 𝐹 ∧ w ⊆ dom 𝐹) → (𝐹 ↾ w) Fn w) |
29 | 18, 27, 28 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐹 ↾ w) Fn w) |
30 | | tfrlem1.3 |
. . . . . . . . . . . . . . . . . 18
⊢ (φ → (Fun 𝐺 ∧ A ⊆ dom 𝐺)) |
31 | 13, 30 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(Fun 𝐺 ∧ A ⊆ dom
𝐺)) |
32 | 31 | simpld 105 |
. . . . . . . . . . . . . . . 16
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) → Fun
𝐺) |
33 | | funfn 4874 |
. . . . . . . . . . . . . . . 16
⊢ (Fun
𝐺 ↔ 𝐺 Fn dom 𝐺) |
34 | 32, 33 | sylib 127 |
. . . . . . . . . . . . . . 15
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
𝐺 Fn dom 𝐺) |
35 | 31 | simprd 107 |
. . . . . . . . . . . . . . . 16
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
A ⊆ dom 𝐺) |
36 | 25, 35 | sstrd 2949 |
. . . . . . . . . . . . . . 15
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
w ⊆ dom 𝐺) |
37 | | fnssres 4955 |
. . . . . . . . . . . . . . 15
⊢ ((𝐺 Fn dom 𝐺 ∧ w ⊆ dom 𝐺) → (𝐺 ↾ w) Fn w) |
38 | 34, 36, 37 | syl2anc 391 |
. . . . . . . . . . . . . 14
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐺 ↾ w) Fn w) |
39 | | simpr 103 |
. . . . . . . . . . . . . . . 16
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
u ∈
w) |
40 | | simplr 482 |
. . . . . . . . . . . . . . . . 17
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
w ∈
y) |
41 | | simplr 482 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) |
42 | 41 | ad2antrr 457 |
. . . . . . . . . . . . . . . . 17
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
∀z
∈ y
(z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) |
43 | 25 | adantr 261 |
. . . . . . . . . . . . . . . . 17
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
w ⊆ A) |
44 | | sseq1 2960 |
. . . . . . . . . . . . . . . . . . 19
⊢ (z = w →
(z ⊆ A ↔ w
⊆ A)) |
45 | | raleq 2499 |
. . . . . . . . . . . . . . . . . . 19
⊢ (z = w →
(∀x
∈ z
(𝐹‘x) = (𝐺‘x) ↔ ∀x ∈ w (𝐹‘x) = (𝐺‘x))) |
46 | 44, 45 | imbi12d 223 |
. . . . . . . . . . . . . . . . . 18
⊢ (z = w →
((z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) ↔ (w
⊆ A → ∀x ∈ w (𝐹‘x) = (𝐺‘x)))) |
47 | 46 | rspcv 2646 |
. . . . . . . . . . . . . . . . 17
⊢ (w ∈ y → (∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (w
⊆ A → ∀x ∈ w (𝐹‘x) = (𝐺‘x)))) |
48 | 40, 42, 43, 47 | syl3c 57 |
. . . . . . . . . . . . . . . 16
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
∀x
∈ w
(𝐹‘x) = (𝐺‘x)) |
49 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = u →
(𝐹‘x) = (𝐹‘u)) |
50 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = u →
(𝐺‘x) = (𝐺‘u)) |
51 | 49, 50 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . 17
⊢ (x = u →
((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘u) = (𝐺‘u))) |
52 | 51 | rspcv 2646 |
. . . . . . . . . . . . . . . 16
⊢ (u ∈ w → (∀x ∈ w (𝐹‘x) = (𝐺‘x) → (𝐹‘u) = (𝐺‘u))) |
53 | 39, 48, 52 | sylc 56 |
. . . . . . . . . . . . . . 15
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
(𝐹‘u) = (𝐺‘u)) |
54 | | fvres 5141 |
. . . . . . . . . . . . . . . 16
⊢ (u ∈ w → ((𝐹 ↾ w)‘u) =
(𝐹‘u)) |
55 | 54 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
((𝐹 ↾ w)‘u) =
(𝐹‘u)) |
56 | | fvres 5141 |
. . . . . . . . . . . . . . . 16
⊢ (u ∈ w → ((𝐺 ↾ w)‘u) =
(𝐺‘u)) |
57 | 56 | adantl 262 |
. . . . . . . . . . . . . . 15
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
((𝐺 ↾ w)‘u) =
(𝐺‘u)) |
58 | 53, 55, 57 | 3eqtr4d 2079 |
. . . . . . . . . . . . . 14
⊢
((((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) ∧ u ∈ w) →
((𝐹 ↾ w)‘u) =
((𝐺 ↾ w)‘u)) |
59 | 29, 38, 58 | eqfnfvd 5211 |
. . . . . . . . . . . . 13
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐹 ↾ w) = (𝐺 ↾ w)) |
60 | 59 | fveq2d 5125 |
. . . . . . . . . . . 12
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(B‘(𝐹 ↾ w)) = (B‘(𝐺 ↾ w))) |
61 | | simpr 103 |
. . . . . . . . . . . . . 14
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ y ⊆ A) |
62 | 61 | sselda 2939 |
. . . . . . . . . . . . 13
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
w ∈
A) |
63 | | tfrlem1.4 |
. . . . . . . . . . . . . 14
⊢ (φ → ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x))) |
64 | 13, 63 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
∀x
∈ A
(𝐹‘x) = (B‘(𝐹 ↾ x))) |
65 | | fveq2 5121 |
. . . . . . . . . . . . . . 15
⊢ (x = w →
(𝐹‘x) = (𝐹‘w)) |
66 | | reseq2 4550 |
. . . . . . . . . . . . . . . 16
⊢ (x = w →
(𝐹 ↾ x) = (𝐹 ↾ w)) |
67 | 66 | fveq2d 5125 |
. . . . . . . . . . . . . . 15
⊢ (x = w →
(B‘(𝐹 ↾ x)) = (B‘(𝐹 ↾ w))) |
68 | 65, 67 | eqeq12d 2051 |
. . . . . . . . . . . . . 14
⊢ (x = w →
((𝐹‘x) = (B‘(𝐹 ↾ x)) ↔ (𝐹‘w) = (B‘(𝐹 ↾ w)))) |
69 | 68 | rspcva 2648 |
. . . . . . . . . . . . 13
⊢
((w ∈ A ∧ ∀x ∈ A (𝐹‘x) = (B‘(𝐹 ↾ x))) → (𝐹‘w) = (B‘(𝐹 ↾ w))) |
70 | 62, 64, 69 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐹‘w) = (B‘(𝐹 ↾ w))) |
71 | | tfrlem1.5 |
. . . . . . . . . . . . . 14
⊢ (φ → ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x))) |
72 | 13, 71 | syl 14 |
. . . . . . . . . . . . 13
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
∀x
∈ A
(𝐺‘x) = (B‘(𝐺 ↾ x))) |
73 | | fveq2 5121 |
. . . . . . . . . . . . . . 15
⊢ (x = w →
(𝐺‘x) = (𝐺‘w)) |
74 | | reseq2 4550 |
. . . . . . . . . . . . . . . 16
⊢ (x = w →
(𝐺 ↾ x) = (𝐺 ↾ w)) |
75 | 74 | fveq2d 5125 |
. . . . . . . . . . . . . . 15
⊢ (x = w →
(B‘(𝐺 ↾ x)) = (B‘(𝐺 ↾ w))) |
76 | 73, 75 | eqeq12d 2051 |
. . . . . . . . . . . . . 14
⊢ (x = w →
((𝐺‘x) = (B‘(𝐺 ↾ x)) ↔ (𝐺‘w) = (B‘(𝐺 ↾ w)))) |
77 | 76 | rspcva 2648 |
. . . . . . . . . . . . 13
⊢
((w ∈ A ∧ ∀x ∈ A (𝐺‘x) = (B‘(𝐺 ↾ x))) → (𝐺‘w) = (B‘(𝐺 ↾ w))) |
78 | 62, 72, 77 | syl2anc 391 |
. . . . . . . . . . . 12
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐺‘w) = (B‘(𝐺 ↾ w))) |
79 | 60, 70, 78 | 3eqtr4d 2079 |
. . . . . . . . . . 11
⊢
(((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
∧ w ∈ y) →
(𝐹‘w) = (𝐺‘w)) |
80 | 79 | ralrimiva 2386 |
. . . . . . . . . 10
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ ∀w ∈ y (𝐹‘w) = (𝐺‘w)) |
81 | 65, 73 | eqeq12d 2051 |
. . . . . . . . . . 11
⊢ (x = w →
((𝐹‘x) = (𝐺‘x) ↔ (𝐹‘w) = (𝐺‘w))) |
82 | 81 | cbvralv 2527 |
. . . . . . . . . 10
⊢ (∀x ∈ y (𝐹‘x) = (𝐺‘x) ↔ ∀w ∈ y (𝐹‘w) = (𝐺‘w)) |
83 | 80, 82 | sylibr 137 |
. . . . . . . . 9
⊢ ((((φ ∧ y ∈ On) ∧ ∀z ∈ y (z ⊆
A → ∀x ∈ z (𝐹‘x) = (𝐺‘x))) ∧ y ⊆ A)
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x)) |
84 | 83 | exp31 346 |
. . . . . . . 8
⊢ ((φ ∧ y ∈ On) →
(∀z
∈ y
(z ⊆ A → ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (y
⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x)))) |
85 | 84 | expcom 109 |
. . . . . . 7
⊢ (y ∈ On →
(φ → (∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x)) → (y
⊆ A → ∀x ∈ y (𝐹‘x) = (𝐺‘x))))) |
86 | 85 | a2d 23 |
. . . . . 6
⊢ (y ∈ On →
((φ → ∀z ∈ y (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) → (φ → (y ⊆ A
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x))))) |
87 | 11, 86 | syl5bi 141 |
. . . . 5
⊢ (y ∈ On →
(∀z
∈ y
(φ → (z ⊆ A
→ ∀x ∈ z (𝐹‘x) = (𝐺‘x))) → (φ → (y ⊆ A
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x))))) |
88 | 10, 87 | tfis2 4251 |
. . . 4
⊢ (y ∈ On →
(φ → (y ⊆ A
→ ∀x ∈ y (𝐹‘x) = (𝐺‘x)))) |
89 | 6, 88 | vtoclga 2613 |
. . 3
⊢ (A ∈ On →
(φ → (A ⊆ A
→ ∀x ∈ A (𝐹‘x) = (𝐺‘x)))) |
90 | 2, 89 | mpcom 32 |
. 2
⊢ (φ → (A ⊆ A
→ ∀x ∈ A (𝐹‘x) = (𝐺‘x))) |
91 | 1, 90 | mpi 15 |
1
⊢ (φ → ∀x ∈ A (𝐹‘x) = (𝐺‘x)) |