ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  tfrlem1 GIF version

Theorem tfrlem1 6055
Description: A technical lemma for transfinite recursion. Compare Lemma 1 of [TakeutiZaring] p. 47. (Contributed by NM, 23-Mar-1995.) (Revised by Mario Carneiro, 24-May-2019.)
Hypotheses
Ref Expression
tfrlem1.1 (𝜑𝐴 ∈ On)
tfrlem1.2 (𝜑 → (Fun 𝐹𝐴 ⊆ dom 𝐹))
tfrlem1.3 (𝜑 → (Fun 𝐺𝐴 ⊆ dom 𝐺))
tfrlem1.4 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐵‘(𝐹𝑥)))
tfrlem1.5 (𝜑 → ∀𝑥𝐴 (𝐺𝑥) = (𝐵‘(𝐺𝑥)))
Assertion
Ref Expression
tfrlem1 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐵   𝑥,𝐹   𝑥,𝐺
Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem tfrlem1
Dummy variables 𝑢 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3042 . 2 𝐴𝐴
2 tfrlem1.1 . . 3 (𝜑𝐴 ∈ On)
3 sseq1 3045 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐴𝐴𝐴))
4 raleq 2562 . . . . . 6 (𝑦 = 𝐴 → (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
53, 4imbi12d 232 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))))
65imbi2d 228 . . . 4 (𝑦 = 𝐴 → ((𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))))
7 sseq1 3045 . . . . . . 7 (𝑦 = 𝑧 → (𝑦𝐴𝑧𝐴))
8 raleq 2562 . . . . . . 7 (𝑦 = 𝑧 → (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))
97, 8imbi12d 232 . . . . . 6 (𝑦 = 𝑧 → ((𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))))
109imbi2d 228 . . . . 5 (𝑦 = 𝑧 → ((𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))))
11 r19.21v 2450 . . . . . 6 (∀𝑧𝑦 (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))))
12 simplll 500 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → 𝜑)
1312adantr 270 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝜑)
14 tfrlem1.2 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Fun 𝐹𝐴 ⊆ dom 𝐹))
1513, 14syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (Fun 𝐹𝐴 ⊆ dom 𝐹))
1615simpld 110 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → Fun 𝐹)
17 funfn 5031 . . . . . . . . . . . . . . . 16 (Fun 𝐹𝐹 Fn dom 𝐹)
1816, 17sylib 120 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐹 Fn dom 𝐹)
19 simpllr 501 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → 𝑦 ∈ On)
20 eloni 4193 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → Ord 𝑦)
2119, 20syl 14 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → Ord 𝑦)
22 ordelss 4197 . . . . . . . . . . . . . . . . . 18 ((Ord 𝑦𝑤𝑦) → 𝑤𝑦)
2321, 22sylan 277 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝑦)
24 simplr 497 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑦𝐴)
2523, 24sstrd 3033 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝐴)
2615simprd 112 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐴 ⊆ dom 𝐹)
2725, 26sstrd 3033 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤 ⊆ dom 𝐹)
28 fnssres 5113 . . . . . . . . . . . . . . 15 ((𝐹 Fn dom 𝐹𝑤 ⊆ dom 𝐹) → (𝐹𝑤) Fn 𝑤)
2918, 27, 28syl2anc 403 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) Fn 𝑤)
30 tfrlem1.3 . . . . . . . . . . . . . . . . . 18 (𝜑 → (Fun 𝐺𝐴 ⊆ dom 𝐺))
3113, 30syl 14 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (Fun 𝐺𝐴 ⊆ dom 𝐺))
3231simpld 110 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → Fun 𝐺)
33 funfn 5031 . . . . . . . . . . . . . . . 16 (Fun 𝐺𝐺 Fn dom 𝐺)
3432, 33sylib 120 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐺 Fn dom 𝐺)
3531simprd 112 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐴 ⊆ dom 𝐺)
3625, 35sstrd 3033 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤 ⊆ dom 𝐺)
37 fnssres 5113 . . . . . . . . . . . . . . 15 ((𝐺 Fn dom 𝐺𝑤 ⊆ dom 𝐺) → (𝐺𝑤) Fn 𝑤)
3834, 36, 37syl2anc 403 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐺𝑤) Fn 𝑤)
39 fveq2 5289 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
40 fveq2 5289 . . . . . . . . . . . . . . . . 17 (𝑥 = 𝑢 → (𝐺𝑥) = (𝐺𝑢))
4139, 40eqeq12d 2102 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → ((𝐹𝑥) = (𝐺𝑥) ↔ (𝐹𝑢) = (𝐺𝑢)))
42 simplr 497 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑤𝑦)
43 simplr 497 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))
4443ad2antrr 472 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))
4525adantr 270 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑤𝐴)
46 sseq1 3045 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (𝑧𝐴𝑤𝐴))
47 raleq 2562 . . . . . . . . . . . . . . . . . . 19 (𝑧 = 𝑤 → (∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥)))
4846, 47imbi12d 232 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → ((𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝑤𝐴 → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥))))
4948rspcv 2718 . . . . . . . . . . . . . . . . 17 (𝑤𝑦 → (∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) → (𝑤𝐴 → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥))))
5042, 44, 45, 49syl3c 62 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥))
51 simpr 108 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑢𝑤)
5241, 50, 51rspcdva 2727 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → (𝐹𝑢) = (𝐺𝑢))
53 fvres 5313 . . . . . . . . . . . . . . . 16 (𝑢𝑤 → ((𝐹𝑤)‘𝑢) = (𝐹𝑢))
5453adantl 271 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐹𝑤)‘𝑢) = (𝐹𝑢))
55 fvres 5313 . . . . . . . . . . . . . . . 16 (𝑢𝑤 → ((𝐺𝑤)‘𝑢) = (𝐺𝑢))
5655adantl 271 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐺𝑤)‘𝑢) = (𝐺𝑢))
5752, 54, 563eqtr4d 2130 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐹𝑤)‘𝑢) = ((𝐺𝑤)‘𝑢))
5829, 38, 57eqfnfvd 5384 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐺𝑤))
5958fveq2d 5293 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐵‘(𝐹𝑤)) = (𝐵‘(𝐺𝑤)))
60 fveq2 5289 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
61 reseq2 4696 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
6261fveq2d 5293 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐵‘(𝐹𝑥)) = (𝐵‘(𝐹𝑤)))
6360, 62eqeq12d 2102 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝐹𝑥) = (𝐵‘(𝐹𝑥)) ↔ (𝐹𝑤) = (𝐵‘(𝐹𝑤))))
64 tfrlem1.4 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐵‘(𝐹𝑥)))
6513, 64syl 14 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → ∀𝑥𝐴 (𝐹𝑥) = (𝐵‘(𝐹𝑥)))
66 simpr 108 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → 𝑦𝐴)
6766sselda 3023 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝐴)
6863, 65, 67rspcdva 2727 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐵‘(𝐹𝑤)))
69 fveq2 5289 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
70 reseq2 4696 . . . . . . . . . . . . . . 15 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
7170fveq2d 5293 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐵‘(𝐺𝑥)) = (𝐵‘(𝐺𝑤)))
7269, 71eqeq12d 2102 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝐵‘(𝐺𝑥)) ↔ (𝐺𝑤) = (𝐵‘(𝐺𝑤))))
73 tfrlem1.5 . . . . . . . . . . . . . 14 (𝜑 → ∀𝑥𝐴 (𝐺𝑥) = (𝐵‘(𝐺𝑥)))
7413, 73syl 14 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → ∀𝑥𝐴 (𝐺𝑥) = (𝐵‘(𝐺𝑥)))
7572, 74, 67rspcdva 2727 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐺𝑤) = (𝐵‘(𝐺𝑤)))
7659, 68, 753eqtr4d 2130 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐺𝑤))
7776ralrimiva 2446 . . . . . . . . . 10 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → ∀𝑤𝑦 (𝐹𝑤) = (𝐺𝑤))
7860, 69eqeq12d 2102 . . . . . . . . . . 11 (𝑥 = 𝑤 → ((𝐹𝑥) = (𝐺𝑥) ↔ (𝐹𝑤) = (𝐺𝑤)))
7978cbvralv 2590 . . . . . . . . . 10 (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑤𝑦 (𝐹𝑤) = (𝐺𝑤))
8077, 79sylibr 132 . . . . . . . . 9 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))
8180exp31 356 . . . . . . . 8 ((𝜑𝑦 ∈ On) → (∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))))
8281expcom 114 . . . . . . 7 (𝑦 ∈ On → (𝜑 → (∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
8382a2d 26 . . . . . 6 (𝑦 ∈ On → ((𝜑 → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) → (𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
8411, 83syl5bi 150 . . . . 5 (𝑦 ∈ On → (∀𝑧𝑦 (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) → (𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
8510, 84tfis2 4390 . . . 4 (𝑦 ∈ On → (𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))))
866, 85vtoclga 2685 . . 3 (𝐴 ∈ On → (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))))
872, 86mpcom 36 . 2 (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
881, 87mpi 15 1 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1289  wcel 1438  wral 2359  wss 2997  Ord word 4180  Oncon0 4181  dom cdm 4428  cres 4430  Fun wfun 4996   Fn wfn 4997  cfv 5002
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-pow 4001  ax-pr 4027  ax-setind 4343
This theorem depends on definitions:  df-bi 115  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-mo 1952  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-rab 2368  df-v 2621  df-sbc 2839  df-csb 2932  df-un 3001  df-in 3003  df-ss 3010  df-pw 3427  df-sn 3447  df-pr 3448  df-op 3450  df-uni 3649  df-br 3838  df-opab 3892  df-mpt 3893  df-tr 3929  df-id 4111  df-iord 4184  df-on 4186  df-xp 4434  df-rel 4435  df-cnv 4436  df-co 4437  df-dm 4438  df-res 4440  df-iota 4967  df-fun 5004  df-fn 5005  df-fv 5010
This theorem is referenced by:  tfrlem5  6061
  Copyright terms: Public domain W3C validator