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

Theorem tfrlem5 5960
Description: Lemma for transfinite recursion. The values of two acceptable functions are the same within their domains. (Contributed by NM, 9-Apr-1995.) (Revised by Mario Carneiro, 24-May-2019.)
Hypothesis
Ref Expression
tfrlem.1 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
Assertion
Ref Expression
tfrlem5 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Distinct variable groups:   𝑓,𝑔,𝑥,𝑦,,𝑢,𝑣,𝐹   𝐴,𝑔,
Allowed substitution hints:   𝐴(𝑥,𝑦,𝑣,𝑢,𝑓)

Proof of Theorem tfrlem5
Dummy variables 𝑧 𝑎 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tfrlem.1 . . 3 𝐴 = {𝑓 ∣ ∃𝑥 ∈ On (𝑓 Fn 𝑥 ∧ ∀𝑦𝑥 (𝑓𝑦) = (𝐹‘(𝑓𝑦)))}
2 vex 2577 . . 3 𝑔 ∈ V
31, 2tfrlem3a 5955 . 2 (𝑔𝐴 ↔ ∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))))
4 vex 2577 . . 3 ∈ V
51, 4tfrlem3a 5955 . 2 (𝐴 ↔ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎))))
6 reeanv 2496 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ↔ (∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))))
7 simp2ll 982 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑔 Fn 𝑧)
8 simp3l 943 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑔𝑢)
9 fnbr 5028 . . . . . . . . . 10 ((𝑔 Fn 𝑧𝑥𝑔𝑢) → 𝑥𝑧)
107, 8, 9syl2anc 397 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑧)
11 simp2rl 984 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fn 𝑤)
12 simp3r 944 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑣)
13 fnbr 5028 . . . . . . . . . 10 (( Fn 𝑤𝑥𝑣) → 𝑥𝑤)
1411, 12, 13syl2anc 397 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥𝑤)
15 elin 3153 . . . . . . . . 9 (𝑥 ∈ (𝑧𝑤) ↔ (𝑥𝑧𝑥𝑤))
1610, 14, 15sylanbrc 402 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑥 ∈ (𝑧𝑤))
17 onin 4150 . . . . . . . . . 10 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (𝑧𝑤) ∈ On)
18173ad2ant1 936 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ∈ On)
19 fnfun 5023 . . . . . . . . . . 11 (𝑔 Fn 𝑧 → Fun 𝑔)
207, 19syl 14 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun 𝑔)
21 inss1 3184 . . . . . . . . . . 11 (𝑧𝑤) ⊆ 𝑧
22 fndm 5025 . . . . . . . . . . . 12 (𝑔 Fn 𝑧 → dom 𝑔 = 𝑧)
237, 22syl 14 . . . . . . . . . . 11 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom 𝑔 = 𝑧)
2421, 23syl5sseqr 3021 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom 𝑔)
2520, 24jca 294 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun 𝑔 ∧ (𝑧𝑤) ⊆ dom 𝑔))
26 fnfun 5023 . . . . . . . . . . 11 ( Fn 𝑤 → Fun )
2711, 26syl 14 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → Fun )
28 inss2 3185 . . . . . . . . . . 11 (𝑧𝑤) ⊆ 𝑤
29 fndm 5025 . . . . . . . . . . . 12 ( Fn 𝑤 → dom = 𝑤)
3011, 29syl 14 . . . . . . . . . . 11 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → dom = 𝑤)
3128, 30syl5sseqr 3021 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑧𝑤) ⊆ dom )
3227, 31jca 294 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (Fun ∧ (𝑧𝑤) ⊆ dom ))
33 simp2lr 983 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)))
34 ssralv 3031 . . . . . . . . . 10 ((𝑧𝑤) ⊆ 𝑧 → (∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎))))
3521, 33, 34mpsyl 63 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝐹‘(𝑔𝑎)))
36 simp2rr 985 . . . . . . . . . 10 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))
37 ssralv 3031 . . . . . . . . . 10 ((𝑧𝑤) ⊆ 𝑤 → (∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎))))
3828, 36, 37mpsyl 63 . . . . . . . . 9 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑎) = (𝐹‘(𝑎)))
3918, 25, 32, 35, 38tfrlem1 5953 . . . . . . . 8 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → ∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎))
40 fveq2 5205 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑔𝑎) = (𝑔𝑥))
41 fveq2 5205 . . . . . . . . . 10 (𝑎 = 𝑥 → (𝑎) = (𝑥))
4240, 41eqeq12d 2070 . . . . . . . . 9 (𝑎 = 𝑥 → ((𝑔𝑎) = (𝑎) ↔ (𝑔𝑥) = (𝑥)))
4342rspcv 2669 . . . . . . . 8 (𝑥 ∈ (𝑧𝑤) → (∀𝑎 ∈ (𝑧𝑤)(𝑔𝑎) = (𝑎) → (𝑔𝑥) = (𝑥)))
4416, 39, 43sylc 60 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = (𝑥))
45 funbrfv 5239 . . . . . . . 8 (Fun 𝑔 → (𝑥𝑔𝑢 → (𝑔𝑥) = 𝑢))
4620, 8, 45sylc 60 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑔𝑥) = 𝑢)
47 funbrfv 5239 . . . . . . . 8 (Fun → (𝑥𝑣 → (𝑥) = 𝑣))
4827, 12, 47sylc 60 . . . . . . 7 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → (𝑥) = 𝑣)
4944, 46, 483eqtr3d 2096 . . . . . 6 (((𝑧 ∈ On ∧ 𝑤 ∈ On) ∧ ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) ∧ (𝑥𝑔𝑢𝑥𝑣)) → 𝑢 = 𝑣)
50493exp 1114 . . . . 5 ((𝑧 ∈ On ∧ 𝑤 ∈ On) → (((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)))
5150rexlimdva 2450 . . . 4 (𝑧 ∈ On → (∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣)))
5251rexlimiv 2444 . . 3 (∃𝑧 ∈ On ∃𝑤 ∈ On ((𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
536, 52sylbir 129 . 2 ((∃𝑧 ∈ On (𝑔 Fn 𝑧 ∧ ∀𝑎𝑧 (𝑔𝑎) = (𝐹‘(𝑔𝑎))) ∧ ∃𝑤 ∈ On ( Fn 𝑤 ∧ ∀𝑎𝑤 (𝑎) = (𝐹‘(𝑎)))) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
543, 5, 53syl2anb 279 1 ((𝑔𝐴𝐴) → ((𝑥𝑔𝑢𝑥𝑣) → 𝑢 = 𝑣))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101  w3a 896   = wceq 1259  wcel 1409  {cab 2042  wral 2323  wrex 2324  cin 2943  wss 2944   class class class wbr 3791  Oncon0 4127  dom cdm 4372  cres 4374  Fun wfun 4923   Fn wfn 4924  cfv 4929
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-14 1421  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3902  ax-pow 3954  ax-pr 3971  ax-setind 4289
This theorem depends on definitions:  df-bi 114  df-3an 898  df-tru 1262  df-nf 1366  df-sb 1662  df-eu 1919  df-mo 1920  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328  df-rex 2329  df-rab 2332  df-v 2576  df-sbc 2787  df-csb 2880  df-un 2949  df-in 2951  df-ss 2958  df-pw 3388  df-sn 3408  df-pr 3409  df-op 3411  df-uni 3608  df-br 3792  df-opab 3846  df-mpt 3847  df-tr 3882  df-id 4057  df-iord 4130  df-on 4132  df-xp 4378  df-rel 4379  df-cnv 4380  df-co 4381  df-dm 4382  df-res 4384  df-iota 4894  df-fun 4931  df-fn 4932  df-fv 4937
This theorem is referenced by:  tfrlem7  5963  tfrexlem  5978
  Copyright terms: Public domain W3C validator