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

Theorem tfr1onlembfn 6013
 Description: Lemma for tfr1on 6019. The union of is a function defined on . (Contributed by Jim Kingdon, 15-Mar-2022.)
Hypotheses
Ref Expression
tfr1on.f recs
tfr1on.g
tfr1on.x
tfr1on.ex
tfr1onlemsucfn.1
tfr1onlembacc.3
tfr1onlembacc.u
tfr1onlembacc.4
tfr1onlembacc.5
Assertion
Ref Expression
tfr1onlembfn
Distinct variable groups:   ,,,,,   ,,,   ,,,   ,,   ,,,,,   ,,   ,,,,   ,,   ,,,,,,   ,,
Allowed substitution hints:   (,)   (,)   (,,)   (,)   (,,,,,,)   ()   (,,)

Proof of Theorem tfr1onlembfn
StepHypRef Expression
1 tfr1on.f . . . . . 6 recs
2 tfr1on.g . . . . . 6
3 tfr1on.x . . . . . 6
4 tfr1on.ex . . . . . 6
5 tfr1onlemsucfn.1 . . . . . 6
6 tfr1onlembacc.3 . . . . . 6
7 tfr1onlembacc.u . . . . . 6
8 tfr1onlembacc.4 . . . . . 6
9 tfr1onlembacc.5 . . . . . 6
101, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembacc 6011 . . . . 5
1110unissd 3645 . . . 4
125, 3tfr1onlemssrecs 6008 . . . 4 recs
1311, 12sstrd 3018 . . 3 recs
14 tfrfun 5989 . . 3 recs
15 funss 4970 . . 3 recs recs
1613, 14, 15mpisyl 1376 . 2
17 simpr3 947 . . . . . . . . . . . 12
18 simpl 107 . . . . . . . . . . . . . . . . . 18
193adantr 270 . . . . . . . . . . . . . . . . . . 19
20 simpr 108 . . . . . . . . . . . . . . . . . . . 20
218adantr 270 . . . . . . . . . . . . . . . . . . . 20
2220, 21jca 300 . . . . . . . . . . . . . . . . . . 19
23 ordtr1 4171 . . . . . . . . . . . . . . . . . . 19
2419, 22, 23sylc 61 . . . . . . . . . . . . . . . . . 18
2518, 24jca 300 . . . . . . . . . . . . . . . . 17
262ad2antrr 472 . . . . . . . . . . . . . . . . . 18
273ad2antrr 472 . . . . . . . . . . . . . . . . . 18
2843adant1r 1163 . . . . . . . . . . . . . . . . . . 19
29283adant1r 1163 . . . . . . . . . . . . . . . . . 18
30 simplr 497 . . . . . . . . . . . . . . . . . 18
31 simpr1 945 . . . . . . . . . . . . . . . . . 18
32 simpr2 946 . . . . . . . . . . . . . . . . . 18
331, 26, 27, 29, 5, 30, 31, 32tfr1onlemsucfn 6009 . . . . . . . . . . . . . . . . 17
3425, 33sylan 277 . . . . . . . . . . . . . . . 16
35 dffn2 5098 . . . . . . . . . . . . . . . 16
3634, 35sylib 120 . . . . . . . . . . . . . . 15
37 fssxp 5109 . . . . . . . . . . . . . . 15
3836, 37syl 14 . . . . . . . . . . . . . 14
39 ordelon 4166 . . . . . . . . . . . . . . . . . . 19
403, 8, 39syl2anc 403 . . . . . . . . . . . . . . . . . 18
41 eloni 4158 . . . . . . . . . . . . . . . . . 18
4240, 41syl 14 . . . . . . . . . . . . . . . . 17
4342ad2antrr 472 . . . . . . . . . . . . . . . 16
44 simplr 497 . . . . . . . . . . . . . . . 16
45 ordsucss 4276 . . . . . . . . . . . . . . . 16
4643, 44, 45sylc 61 . . . . . . . . . . . . . . 15
47 xpss1 4496 . . . . . . . . . . . . . . 15
4846, 47syl 14 . . . . . . . . . . . . . 14
4938, 48sstrd 3018 . . . . . . . . . . . . 13
50 vex 2613 . . . . . . . . . . . . . . 15
51 vex 2613 . . . . . . . . . . . . . . . . 17
5218adantr 270 . . . . . . . . . . . . . . . . . 18
5324adantr 270 . . . . . . . . . . . . . . . . . 18
54 simpr1 945 . . . . . . . . . . . . . . . . . 18
55 fneq2 5039 . . . . . . . . . . . . . . . . . . . . . 22
5655imbi1d 229 . . . . . . . . . . . . . . . . . . . . 21
5756albidv 1747 . . . . . . . . . . . . . . . . . . . 20
5843expia 1141 . . . . . . . . . . . . . . . . . . . . . . 23
5958alrimiv 1797 . . . . . . . . . . . . . . . . . . . . . 22
6059ralrimiva 2439 . . . . . . . . . . . . . . . . . . . . 21
61603ad2ant1 960 . . . . . . . . . . . . . . . . . . . 20
62 simp2 940 . . . . . . . . . . . . . . . . . . . 20
6357, 61, 62rspcdva 2715 . . . . . . . . . . . . . . . . . . 19
64 simp3 941 . . . . . . . . . . . . . . . . . . 19
65 fneq1 5038 . . . . . . . . . . . . . . . . . . . . 21
66 fveq2 5229 . . . . . . . . . . . . . . . . . . . . . 22
6766eleq1d 2151 . . . . . . . . . . . . . . . . . . . . 21
6865, 67imbi12d 232 . . . . . . . . . . . . . . . . . . . 20
6968spv 1783 . . . . . . . . . . . . . . . . . . 19
7063, 64, 69sylc 61 . . . . . . . . . . . . . . . . . 18
7152, 53, 54, 70syl3anc 1170 . . . . . . . . . . . . . . . . 17
72 opexg 4011 . . . . . . . . . . . . . . . . 17
7351, 71, 72sylancr 405 . . . . . . . . . . . . . . . 16
74 snexg 3976 . . . . . . . . . . . . . . . 16
7573, 74syl 14 . . . . . . . . . . . . . . 15
76 unexg 4224 . . . . . . . . . . . . . . 15
7750, 75, 76sylancr 405 . . . . . . . . . . . . . 14
78 elpwg 3408 . . . . . . . . . . . . . 14
7977, 78syl 14 . . . . . . . . . . . . 13
8049, 79mpbird 165 . . . . . . . . . . . 12
8117, 80eqeltrd 2159 . . . . . . . . . . 11
8281ex 113 . . . . . . . . . 10
8382exlimdv 1742 . . . . . . . . 9
8483rexlimdva 2482 . . . . . . . 8
8584abssdv 3077 . . . . . . 7
866, 85syl5eqss 3052 . . . . . 6
87 sspwuni 3780 . . . . . 6
8886, 87sylib 120 . . . . 5
89 dmss 4582 . . . . 5
9088, 89syl 14 . . . 4
91 dmxpss 4803 . . . 4
9290, 91syl6ss 3020 . . 3
931, 2, 3, 4, 5, 6, 7, 8, 9tfr1onlembxssdm 6012 . . 3
9492, 93eqssd 3025 . 2
95 df-fn 4955 . 2
9616, 94, 95sylanbrc 408 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 102   wb 103   w3a 920  wal 1283   wceq 1285  wex 1422   wcel 1434  cab 2069  wral 2353  wrex 2354  cvv 2610   cun 2980   wss 2982  cpw 3400  csn 3416  cop 3419  cuni 3621   word 4145  con0 4146   csuc 4148   cxp 4389   cdm 4391   cres 4393   wfun 4946   wfn 4947  wf 4948  cfv 4952  recscrecs 5973 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-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3916  ax-pow 3968  ax-pr 3992  ax-un 4216  ax-setind 4308 This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-fal 1291  df-nf 1391  df-sb 1688  df-eu 1946  df-mo 1947  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ne 2250  df-ral 2358  df-rex 2359  df-rab 2362  df-v 2612  df-sbc 2825  df-csb 2918  df-dif 2984  df-un 2986  df-in 2988  df-ss 2995  df-nul 3268  df-pw 3402  df-sn 3422  df-pr 3423  df-op 3425  df-uni 3622  df-iun 3700  df-br 3806  df-opab 3860  df-mpt 3861  df-tr 3896  df-id 4076  df-iord 4149  df-on 4151  df-suc 4154  df-xp 4397  df-rel 4398  df-cnv 4399  df-co 4400  df-dm 4401  df-rn 4402  df-res 4403  df-iota 4917  df-fun 4954  df-fn 4955  df-f 4956  df-fv 4960  df-recs 5974 This theorem is referenced by:  tfr1onlembex  6014  tfr1onlemubacc  6015  tfr1onlemex  6016
 Copyright terms: Public domain W3C validator