MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tfrlem1 Structured version   Visualization version   GIF version

Theorem tfrlem1 7755
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 3841 . 2 𝐴𝐴
2 tfrlem1.1 . . 3 (𝜑𝐴 ∈ On)
3 sseq1 3844 . . . . . 6 (𝑦 = 𝑧 → (𝑦𝐴𝑧𝐴))
4 raleq 3329 . . . . . 6 (𝑦 = 𝑧 → (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))
53, 4imbi12d 336 . . . . 5 (𝑦 = 𝑧 → ((𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))))
65imbi2d 332 . . . 4 (𝑦 = 𝑧 → ((𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))))
7 sseq1 3844 . . . . . 6 (𝑦 = 𝐴 → (𝑦𝐴𝐴𝐴))
8 raleq 3329 . . . . . 6 (𝑦 = 𝐴 → (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
97, 8imbi12d 336 . . . . 5 (𝑦 = 𝐴 → ((𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))))
109imbi2d 332 . . . 4 (𝑦 = 𝐴 → ((𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))))
11 r19.21v 3141 . . . . 5 (∀𝑧𝑦 (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ↔ (𝜑 → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))))
12 tfrlem1.2 . . . . . . . . . . . . . . . . 17 (𝜑 → (Fun 𝐹𝐴 ⊆ dom 𝐹))
1312ad4antr 722 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (Fun 𝐹𝐴 ⊆ dom 𝐹))
1413simpld 490 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → Fun 𝐹)
1514funfnd 6166 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐹 Fn dom 𝐹)
16 eloni 5986 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ On → Ord 𝑦)
1716ad3antlr 721 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → Ord 𝑦)
18 ordelss 5992 . . . . . . . . . . . . . . . . 17 ((Ord 𝑦𝑤𝑦) → 𝑤𝑦)
1917, 18sylan 575 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝑦)
20 simplr 759 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑦𝐴)
2119, 20sstrd 3830 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝐴)
2213simprd 491 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐴 ⊆ dom 𝐹)
2321, 22sstrd 3830 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤 ⊆ dom 𝐹)
24 fnssres 6250 . . . . . . . . . . . . . 14 ((𝐹 Fn dom 𝐹𝑤 ⊆ dom 𝐹) → (𝐹𝑤) Fn 𝑤)
2515, 23, 24syl2anc 579 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) Fn 𝑤)
26 tfrlem1.3 . . . . . . . . . . . . . . . . 17 (𝜑 → (Fun 𝐺𝐴 ⊆ dom 𝐺))
2726ad4antr 722 . . . . . . . . . . . . . . . 16 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (Fun 𝐺𝐴 ⊆ dom 𝐺))
2827simpld 490 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → Fun 𝐺)
2928funfnd 6166 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐺 Fn dom 𝐺)
3027simprd 491 . . . . . . . . . . . . . . 15 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝐴 ⊆ dom 𝐺)
3121, 30sstrd 3830 . . . . . . . . . . . . . 14 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤 ⊆ dom 𝐺)
32 fnssres 6250 . . . . . . . . . . . . . 14 ((𝐺 Fn dom 𝐺𝑤 ⊆ dom 𝐺) → (𝐺𝑤) Fn 𝑤)
3329, 31, 32syl2anc 579 . . . . . . . . . . . . 13 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐺𝑤) Fn 𝑤)
34 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → (𝐹𝑥) = (𝐹𝑢))
35 fveq2 6446 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → (𝐺𝑥) = (𝐺𝑢))
3634, 35eqeq12d 2792 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → ((𝐹𝑥) = (𝐺𝑥) ↔ (𝐹𝑢) = (𝐺𝑢)))
3721adantr 474 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑤𝐴)
38 sseq1 3844 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (𝑧𝐴𝑤𝐴))
39 raleq 3329 . . . . . . . . . . . . . . . . . 18 (𝑧 = 𝑤 → (∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥)))
4038, 39imbi12d 336 . . . . . . . . . . . . . . . . 17 (𝑧 = 𝑤 → ((𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) ↔ (𝑤𝐴 → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥))))
41 simp-4r 774 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)))
42 simplr 759 . . . . . . . . . . . . . . . . 17 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑤𝑦)
4340, 41, 42rspcdva 3516 . . . . . . . . . . . . . . . 16 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → (𝑤𝐴 → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥)))
4437, 43mpd 15 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ∀𝑥𝑤 (𝐹𝑥) = (𝐺𝑥))
45 simpr 479 . . . . . . . . . . . . . . 15 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → 𝑢𝑤)
4636, 44, 45rspcdva 3516 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → (𝐹𝑢) = (𝐺𝑢))
47 fvres 6465 . . . . . . . . . . . . . . 15 (𝑢𝑤 → ((𝐹𝑤)‘𝑢) = (𝐹𝑢))
4847adantl 475 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐹𝑤)‘𝑢) = (𝐹𝑢))
49 fvres 6465 . . . . . . . . . . . . . . 15 (𝑢𝑤 → ((𝐺𝑤)‘𝑢) = (𝐺𝑢))
5049adantl 475 . . . . . . . . . . . . . 14 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐺𝑤)‘𝑢) = (𝐺𝑢))
5146, 48, 503eqtr4d 2823 . . . . . . . . . . . . 13 ((((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) ∧ 𝑢𝑤) → ((𝐹𝑤)‘𝑢) = ((𝐺𝑤)‘𝑢))
5225, 33, 51eqfnfvd 6577 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐺𝑤))
5352fveq2d 6450 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐵‘(𝐹𝑤)) = (𝐵‘(𝐺𝑤)))
54 fveq2 6446 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
55 reseq2 5637 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐹𝑥) = (𝐹𝑤))
5655fveq2d 6450 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵‘(𝐹𝑥)) = (𝐵‘(𝐹𝑤)))
5754, 56eqeq12d 2792 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐹𝑥) = (𝐵‘(𝐹𝑥)) ↔ (𝐹𝑤) = (𝐵‘(𝐹𝑤))))
58 tfrlem1.4 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐵‘(𝐹𝑥)))
5958ad4antr 722 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → ∀𝑥𝐴 (𝐹𝑥) = (𝐵‘(𝐹𝑥)))
60 simpr 479 . . . . . . . . . . . . 13 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → 𝑦𝐴)
6160sselda 3820 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → 𝑤𝐴)
6257, 59, 61rspcdva 3516 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐵‘(𝐹𝑤)))
63 fveq2 6446 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
64 reseq2 5637 . . . . . . . . . . . . . 14 (𝑥 = 𝑤 → (𝐺𝑥) = (𝐺𝑤))
6564fveq2d 6450 . . . . . . . . . . . . 13 (𝑥 = 𝑤 → (𝐵‘(𝐺𝑥)) = (𝐵‘(𝐺𝑤)))
6663, 65eqeq12d 2792 . . . . . . . . . . . 12 (𝑥 = 𝑤 → ((𝐺𝑥) = (𝐵‘(𝐺𝑥)) ↔ (𝐺𝑤) = (𝐵‘(𝐺𝑤))))
67 tfrlem1.5 . . . . . . . . . . . . 13 (𝜑 → ∀𝑥𝐴 (𝐺𝑥) = (𝐵‘(𝐺𝑥)))
6867ad4antr 722 . . . . . . . . . . . 12 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → ∀𝑥𝐴 (𝐺𝑥) = (𝐵‘(𝐺𝑥)))
6966, 68, 61rspcdva 3516 . . . . . . . . . . 11 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐺𝑤) = (𝐵‘(𝐺𝑤)))
7053, 62, 693eqtr4d 2823 . . . . . . . . . 10 (((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) ∧ 𝑤𝑦) → (𝐹𝑤) = (𝐺𝑤))
7170ralrimiva 3147 . . . . . . . . 9 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → ∀𝑤𝑦 (𝐹𝑤) = (𝐺𝑤))
7254, 63eqeq12d 2792 . . . . . . . . . 10 (𝑥 = 𝑤 → ((𝐹𝑥) = (𝐺𝑥) ↔ (𝐹𝑤) = (𝐺𝑤)))
7372cbvralv 3366 . . . . . . . . 9 (∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥) ↔ ∀𝑤𝑦 (𝐹𝑤) = (𝐺𝑤))
7471, 73sylibr 226 . . . . . . . 8 ((((𝜑𝑦 ∈ On) ∧ ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) ∧ 𝑦𝐴) → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))
7574exp31 412 . . . . . . 7 ((𝜑𝑦 ∈ On) → (∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥))))
7675expcom 404 . . . . . 6 (𝑦 ∈ On → (𝜑 → (∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥)) → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
7776a2d 29 . . . . 5 (𝑦 ∈ On → ((𝜑 → ∀𝑧𝑦 (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) → (𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
7811, 77syl5bi 234 . . . 4 (𝑦 ∈ On → (∀𝑧𝑦 (𝜑 → (𝑧𝐴 → ∀𝑥𝑧 (𝐹𝑥) = (𝐺𝑥))) → (𝜑 → (𝑦𝐴 → ∀𝑥𝑦 (𝐹𝑥) = (𝐺𝑥)))))
796, 10, 78tfis3 7335 . . 3 (𝐴 ∈ On → (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))))
802, 79mpcom 38 . 2 (𝜑 → (𝐴𝐴 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥)))
811, 80mpi 20 1 (𝜑 → ∀𝑥𝐴 (𝐹𝑥) = (𝐺𝑥))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386   = wceq 1601  wcel 2106  wral 3089  wss 3791  dom cdm 5355  cres 5357  Ord word 5975  Oncon0 5976  Fun wfun 6129   Fn wfn 6130  cfv 6135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-8 2108  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-csb 3751  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-pss 3807  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-tp 4402  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-iota 6099  df-fun 6137  df-fn 6138  df-fv 6143
This theorem is referenced by:  tfrlem5  7759
  Copyright terms: Public domain W3C validator