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

Theorem tfrlem1 5841
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 (φA On)
tfrlem1.2 (φ → (Fun 𝐹 A ⊆ dom 𝐹))
tfrlem1.3 (φ → (Fun 𝐺 A ⊆ dom 𝐺))
tfrlem1.4 (φx A (𝐹x) = (B‘(𝐹x)))
tfrlem1.5 (φx A (𝐺x) = (B‘(𝐺x)))
Assertion
Ref Expression
tfrlem1 (φx A (𝐹x) = (𝐺x))
Distinct variable groups:   x,A   x,B   x,𝐹   x,𝐺
Allowed substitution hint:   φ(x)

Proof of Theorem tfrlem1
Dummy variables u w y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 2937 . 2 AA
2 tfrlem1.1 . . 3 (φA On)
3 sseq1 2939 . . . . . 6 (y = A → (yAAA))
4 raleq 2479 . . . . . 6 (y = A → (x y (𝐹x) = (𝐺x) ↔ x A (𝐹x) = (𝐺x)))
53, 4imbi12d 223 . . . . 5 (y = A → ((yAx y (𝐹x) = (𝐺x)) ↔ (AAx A (𝐹x) = (𝐺x))))
65imbi2d 219 . . . 4 (y = A → ((φ → (yAx y (𝐹x) = (𝐺x))) ↔ (φ → (AAx A (𝐹x) = (𝐺x)))))
7 sseq1 2939 . . . . . . 7 (y = z → (yAzA))
8 raleq 2479 . . . . . . 7 (y = z → (x y (𝐹x) = (𝐺x) ↔ x z (𝐹x) = (𝐺x)))
97, 8imbi12d 223 . . . . . 6 (y = z → ((yAx y (𝐹x) = (𝐺x)) ↔ (zAx z (𝐹x) = (𝐺x))))
109imbi2d 219 . . . . 5 (y = z → ((φ → (yAx y (𝐹x) = (𝐺x))) ↔ (φ → (zAx z (𝐹x) = (𝐺x)))))
11 r19.21v 2370 . . . . . 6 (z y (φ → (zAx z (𝐹x) = (𝐺x))) ↔ (φz y (zAx z (𝐹x) = (𝐺x))))
12 simplll 473 . . . . . . . . . . . . . . . . . . 19 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → φ)
1312adantr 261 . . . . . . . . . . . . . . . . . 18 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → φ)
14 tfrlem1.2 . . . . . . . . . . . . . . . . . 18 (φ → (Fun 𝐹 A ⊆ dom 𝐹))
1513, 14syl 14 . . . . . . . . . . . . . . . . 17 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (Fun 𝐹 A ⊆ dom 𝐹))
1615simpld 105 . . . . . . . . . . . . . . . 16 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → Fun 𝐹)
17 funfn 4853 . . . . . . . . . . . . . . . 16 (Fun 𝐹𝐹 Fn dom 𝐹)
1816, 17sylib 127 . . . . . . . . . . . . . . 15 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → 𝐹 Fn dom 𝐹)
19 simpllr 474 . . . . . . . . . . . . . . . . . . 19 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → y On)
20 eloni 4057 . . . . . . . . . . . . . . . . . . 19 (y On → Ord y)
2119, 20syl 14 . . . . . . . . . . . . . . . . . 18 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → Ord y)
22 ordelss 4061 . . . . . . . . . . . . . . . . . 18 ((Ord y w y) → wy)
2321, 22sylan 267 . . . . . . . . . . . . . . . . 17 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → wy)
24 simplr 470 . . . . . . . . . . . . . . . . 17 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → yA)
2523, 24sstrd 2928 . . . . . . . . . . . . . . . 16 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → wA)
2615simprd 107 . . . . . . . . . . . . . . . 16 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → A ⊆ dom 𝐹)
2725, 26sstrd 2928 . . . . . . . . . . . . . . 15 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → w ⊆ dom 𝐹)
28 fnssres 4934 . . . . . . . . . . . . . . 15 ((𝐹 Fn dom 𝐹 w ⊆ dom 𝐹) → (𝐹w) Fn w)
2918, 27, 28syl2anc 393 . . . . . . . . . . . . . 14 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐹w) Fn w)
30 tfrlem1.3 . . . . . . . . . . . . . . . . . 18 (φ → (Fun 𝐺 A ⊆ dom 𝐺))
3113, 30syl 14 . . . . . . . . . . . . . . . . 17 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (Fun 𝐺 A ⊆ dom 𝐺))
3231simpld 105 . . . . . . . . . . . . . . . 16 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → Fun 𝐺)
33 funfn 4853 . . . . . . . . . . . . . . . 16 (Fun 𝐺𝐺 Fn dom 𝐺)
3432, 33sylib 127 . . . . . . . . . . . . . . 15 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → 𝐺 Fn dom 𝐺)
3531simprd 107 . . . . . . . . . . . . . . . 16 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → A ⊆ dom 𝐺)
3625, 35sstrd 2928 . . . . . . . . . . . . . . 15 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → w ⊆ dom 𝐺)
37 fnssres 4934 . . . . . . . . . . . . . . 15 ((𝐺 Fn dom 𝐺 w ⊆ dom 𝐺) → (𝐺w) Fn w)
3834, 36, 37syl2anc 393 . . . . . . . . . . . . . 14 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐺w) Fn w)
39 simpr 103 . . . . . . . . . . . . . . . 16 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → u w)
40 simplr 470 . . . . . . . . . . . . . . . . 17 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → w y)
41 simplr 470 . . . . . . . . . . . . . . . . . 18 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → z y (zAx z (𝐹x) = (𝐺x)))
4241ad2antrr 460 . . . . . . . . . . . . . . . . 17 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → z y (zAx z (𝐹x) = (𝐺x)))
4325adantr 261 . . . . . . . . . . . . . . . . 17 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → wA)
44 sseq1 2939 . . . . . . . . . . . . . . . . . . 19 (z = w → (zAwA))
45 raleq 2479 . . . . . . . . . . . . . . . . . . 19 (z = w → (x z (𝐹x) = (𝐺x) ↔ x w (𝐹x) = (𝐺x)))
4644, 45imbi12d 223 . . . . . . . . . . . . . . . . . 18 (z = w → ((zAx z (𝐹x) = (𝐺x)) ↔ (wAx w (𝐹x) = (𝐺x))))
4746rspcv 2625 . . . . . . . . . . . . . . . . 17 (w y → (z y (zAx z (𝐹x) = (𝐺x)) → (wAx w (𝐹x) = (𝐺x))))
4840, 42, 43, 47syl3c 57 . . . . . . . . . . . . . . . 16 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → x w (𝐹x) = (𝐺x))
49 fveq2 5099 . . . . . . . . . . . . . . . . . 18 (x = u → (𝐹x) = (𝐹u))
50 fveq2 5099 . . . . . . . . . . . . . . . . . 18 (x = u → (𝐺x) = (𝐺u))
5149, 50eqeq12d 2032 . . . . . . . . . . . . . . . . 17 (x = u → ((𝐹x) = (𝐺x) ↔ (𝐹u) = (𝐺u)))
5251rspcv 2625 . . . . . . . . . . . . . . . 16 (u w → (x w (𝐹x) = (𝐺x) → (𝐹u) = (𝐺u)))
5339, 48, 52sylc 56 . . . . . . . . . . . . . . 15 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → (𝐹u) = (𝐺u))
54 fvres 5119 . . . . . . . . . . . . . . . 16 (u w → ((𝐹w)‘u) = (𝐹u))
5554adantl 262 . . . . . . . . . . . . . . 15 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → ((𝐹w)‘u) = (𝐹u))
56 fvres 5119 . . . . . . . . . . . . . . . 16 (u w → ((𝐺w)‘u) = (𝐺u))
5756adantl 262 . . . . . . . . . . . . . . 15 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → ((𝐺w)‘u) = (𝐺u))
5853, 55, 573eqtr4d 2060 . . . . . . . . . . . . . 14 ((((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) u w) → ((𝐹w)‘u) = ((𝐺w)‘u))
5929, 38, 58eqfnfvd 5189 . . . . . . . . . . . . 13 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐹w) = (𝐺w))
6059fveq2d 5103 . . . . . . . . . . . 12 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (B‘(𝐹w)) = (B‘(𝐺w)))
61 simpr 103 . . . . . . . . . . . . . 14 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → yA)
6261sselda 2918 . . . . . . . . . . . . 13 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → w A)
63 tfrlem1.4 . . . . . . . . . . . . . 14 (φx A (𝐹x) = (B‘(𝐹x)))
6413, 63syl 14 . . . . . . . . . . . . 13 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → x A (𝐹x) = (B‘(𝐹x)))
65 fveq2 5099 . . . . . . . . . . . . . . 15 (x = w → (𝐹x) = (𝐹w))
66 reseq2 4530 . . . . . . . . . . . . . . . 16 (x = w → (𝐹x) = (𝐹w))
6766fveq2d 5103 . . . . . . . . . . . . . . 15 (x = w → (B‘(𝐹x)) = (B‘(𝐹w)))
6865, 67eqeq12d 2032 . . . . . . . . . . . . . 14 (x = w → ((𝐹x) = (B‘(𝐹x)) ↔ (𝐹w) = (B‘(𝐹w))))
6968rspcva 2627 . . . . . . . . . . . . 13 ((w A x A (𝐹x) = (B‘(𝐹x))) → (𝐹w) = (B‘(𝐹w)))
7062, 64, 69syl2anc 393 . . . . . . . . . . . 12 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐹w) = (B‘(𝐹w)))
71 tfrlem1.5 . . . . . . . . . . . . . 14 (φx A (𝐺x) = (B‘(𝐺x)))
7213, 71syl 14 . . . . . . . . . . . . 13 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → x A (𝐺x) = (B‘(𝐺x)))
73 fveq2 5099 . . . . . . . . . . . . . . 15 (x = w → (𝐺x) = (𝐺w))
74 reseq2 4530 . . . . . . . . . . . . . . . 16 (x = w → (𝐺x) = (𝐺w))
7574fveq2d 5103 . . . . . . . . . . . . . . 15 (x = w → (B‘(𝐺x)) = (B‘(𝐺w)))
7673, 75eqeq12d 2032 . . . . . . . . . . . . . 14 (x = w → ((𝐺x) = (B‘(𝐺x)) ↔ (𝐺w) = (B‘(𝐺w))))
7776rspcva 2627 . . . . . . . . . . . . 13 ((w A x A (𝐺x) = (B‘(𝐺x))) → (𝐺w) = (B‘(𝐺w)))
7862, 72, 77syl2anc 393 . . . . . . . . . . . 12 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐺w) = (B‘(𝐺w)))
7960, 70, 783eqtr4d 2060 . . . . . . . . . . 11 (((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) w y) → (𝐹w) = (𝐺w))
8079ralrimiva 2366 . . . . . . . . . 10 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → w y (𝐹w) = (𝐺w))
8165, 73eqeq12d 2032 . . . . . . . . . . 11 (x = w → ((𝐹x) = (𝐺x) ↔ (𝐹w) = (𝐺w)))
8281cbvralv 2507 . . . . . . . . . 10 (x y (𝐹x) = (𝐺x) ↔ w y (𝐹w) = (𝐺w))
8380, 82sylibr 137 . . . . . . . . 9 ((((φ y On) z y (zAx z (𝐹x) = (𝐺x))) yA) → x y (𝐹x) = (𝐺x))
8483exp31 346 . . . . . . . 8 ((φ y On) → (z y (zAx z (𝐹x) = (𝐺x)) → (yAx y (𝐹x) = (𝐺x))))
8584expcom 109 . . . . . . 7 (y On → (φ → (z y (zAx z (𝐹x) = (𝐺x)) → (yAx y (𝐹x) = (𝐺x)))))
8685a2d 23 . . . . . 6 (y On → ((φz y (zAx z (𝐹x) = (𝐺x))) → (φ → (yAx y (𝐹x) = (𝐺x)))))
8711, 86syl5bi 141 . . . . 5 (y On → (z y (φ → (zAx z (𝐹x) = (𝐺x))) → (φ → (yAx y (𝐹x) = (𝐺x)))))
8810, 87tfis2 4231 . . . 4 (y On → (φ → (yAx y (𝐹x) = (𝐺x))))
896, 88vtoclga 2592 . . 3 (A On → (φ → (AAx A (𝐹x) = (𝐺x))))
902, 89mpcom 32 . 2 (φ → (AAx A (𝐹x) = (𝐺x)))
911, 90mpi 15 1 (φx A (𝐹x) = (𝐺x))
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   = wceq 1226   wcel 1370  wral 2280  wss 2890  Ord word 4044  Oncon0 4045  dom cdm 4268  cres 4270  Fun wfun 4819   Fn wfn 4820  cfv 4825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 617  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-10 1373  ax-11 1374  ax-i12 1375  ax-bnd 1376  ax-4 1377  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-sep 3845  ax-pow 3897  ax-pr 3914  ax-setind 4200
This theorem depends on definitions:  df-bi 110  df-3an 873  df-tru 1229  df-nf 1326  df-sb 1624  df-eu 1881  df-mo 1882  df-clab 2005  df-cleq 2011  df-clel 2014  df-nfc 2145  df-ral 2285  df-rex 2286  df-rab 2289  df-v 2533  df-sbc 2738  df-csb 2826  df-un 2895  df-in 2897  df-ss 2904  df-pw 3332  df-sn 3352  df-pr 3353  df-op 3355  df-uni 3551  df-br 3735  df-opab 3789  df-mpt 3790  df-tr 3825  df-id 4000  df-iord 4048  df-on 4050  df-xp 4274  df-rel 4275  df-cnv 4276  df-co 4277  df-dm 4278  df-res 4280  df-iota 4790  df-fun 4827  df-fn 4828  df-fv 4833
This theorem is referenced by:  tfrlem5  5848
  Copyright terms: Public domain W3C validator