Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >   Mathboxes  >  bj-findis Structured version   GIF version

Theorem bj-findis 7393
Description: Principle of induction, using implicit substitutions (the biconditional versions of the hypotheses are implicit substitutions, and we have weakened them to implications). Constructive proof (from CZF). See bj-bdfindis 7365 for a bounded version not requiring ax-setind 4200. See finds 4246 for a proof in IZF. From this version, it is easy to prove of finds 4246, finds2 4247, finds1 4248. (Contributed by BJ, 22-Dec-2019.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
bj-findis.nf0 xψ
bj-findis.nf1 xχ
bj-findis.nfsuc xθ
bj-findis.0 (x = ∅ → (ψφ))
bj-findis.1 (x = y → (φχ))
bj-findis.suc (x = suc y → (θφ))
Assertion
Ref Expression
bj-findis ((ψ y 𝜔 (χθ)) → x 𝜔 φ)
Distinct variable groups:   x,y   φ,y
Allowed substitution hints:   φ(x)   ψ(x,y)   χ(x,y)   θ(x,y)

Proof of Theorem bj-findis
Dummy variable z is distinct from all other variables.
StepHypRef Expression
1 bj-nn0suc 7378 . . . . 5 (z 𝜔 ↔ (z = ∅ y 𝜔 z = suc y))
2 pm3.21 251 . . . . . . . 8 (ψ → (z = ∅ → (z = ∅ ψ)))
32ad2antrr 460 . . . . . . 7 (((ψ y 𝜔 (χθ)) y z (y 𝜔 → χ)) → (z = ∅ → (z = ∅ ψ)))
4 pm2.04 76 . . . . . . . . . . 11 ((y z → (y 𝜔 → χ)) → (y 𝜔 → (y zχ)))
54ralimi2 2355 . . . . . . . . . 10 (y z (y 𝜔 → χ) → y 𝜔 (y zχ))
6 imim2 49 . . . . . . . . . . . 12 ((χθ) → ((y zχ) → (y zθ)))
76ral2imi 2359 . . . . . . . . . . 11 (y 𝜔 (χθ) → (y 𝜔 (y zχ) → y 𝜔 (y zθ)))
87imp 115 . . . . . . . . . 10 ((y 𝜔 (χθ) y 𝜔 (y zχ)) → y 𝜔 (y zθ))
95, 8sylan2 270 . . . . . . . . 9 ((y 𝜔 (χθ) y z (y 𝜔 → χ)) → y 𝜔 (y zθ))
10 r19.29 2424 . . . . . . . . . . 11 ((y 𝜔 (y zθ) y 𝜔 z = suc y) → y 𝜔 ((y zθ) z = suc y))
11 vex 2534 . . . . . . . . . . . . . . . 16 y V
1211sucid 4099 . . . . . . . . . . . . . . 15 y suc y
13 eleq2 2079 . . . . . . . . . . . . . . 15 (z = suc y → (y zy suc y))
1412, 13mpbiri 157 . . . . . . . . . . . . . 14 (z = suc yy z)
15 ax-1 5 . . . . . . . . . . . . . . 15 (z = suc y → ((y zθ) → z = suc y))
16 pm2.27 35 . . . . . . . . . . . . . . 15 (y z → ((y zθ) → θ))
1715, 16anim12ii 325 . . . . . . . . . . . . . 14 ((z = suc y y z) → ((y zθ) → (z = suc y θ)))
1814, 17mpdan 400 . . . . . . . . . . . . 13 (z = suc y → ((y zθ) → (z = suc y θ)))
1918impcom 116 . . . . . . . . . . . 12 (((y zθ) z = suc y) → (z = suc y θ))
2019reximi 2390 . . . . . . . . . . 11 (y 𝜔 ((y zθ) z = suc y) → y 𝜔 (z = suc y θ))
2110, 20syl 14 . . . . . . . . . 10 ((y 𝜔 (y zθ) y 𝜔 z = suc y) → y 𝜔 (z = suc y θ))
2221ex 108 . . . . . . . . 9 (y 𝜔 (y zθ) → (y 𝜔 z = suc yy 𝜔 (z = suc y θ)))
239, 22syl 14 . . . . . . . 8 ((y 𝜔 (χθ) y z (y 𝜔 → χ)) → (y 𝜔 z = suc yy 𝜔 (z = suc y θ)))
2423adantll 448 . . . . . . 7 (((ψ y 𝜔 (χθ)) y z (y 𝜔 → χ)) → (y 𝜔 z = suc yy 𝜔 (z = suc y θ)))
253, 24orim12d 687 . . . . . 6 (((ψ y 𝜔 (χθ)) y z (y 𝜔 → χ)) → ((z = ∅ y 𝜔 z = suc y) → ((z = ∅ ψ) y 𝜔 (z = suc y θ))))
2625ex 108 . . . . 5 ((ψ y 𝜔 (χθ)) → (y z (y 𝜔 → χ) → ((z = ∅ y 𝜔 z = suc y) → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))))
271, 26syl7bi 154 . . . 4 ((ψ y 𝜔 (χθ)) → (y z (y 𝜔 → χ) → (z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))))
2827alrimiv 1732 . . 3 ((ψ y 𝜔 (χθ)) → z(y z (y 𝜔 → χ) → (z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))))
29 nfv 1398 . . . . 5 x y 𝜔
30 bj-findis.nf1 . . . . 5 xχ
3129, 30nfim 1442 . . . 4 x(y 𝜔 → χ)
32 nfv 1398 . . . . 5 x z 𝜔
33 nfv 1398 . . . . . . 7 x z = ∅
34 bj-findis.nf0 . . . . . . 7 xψ
3533, 34nfan 1435 . . . . . 6 x(z = ∅ ψ)
36 nfcv 2156 . . . . . . 7 x𝜔
37 nfv 1398 . . . . . . . 8 x z = suc y
38 bj-findis.nfsuc . . . . . . . 8 xθ
3937, 38nfan 1435 . . . . . . 7 x(z = suc y θ)
4036, 39nfrexxy 2335 . . . . . 6 xy 𝜔 (z = suc y θ)
4135, 40nfor 1444 . . . . 5 x((z = ∅ ψ) y 𝜔 (z = suc y θ))
4232, 41nfim 1442 . . . 4 x(z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))
43 nfv 1398 . . . 4 z(x 𝜔 → φ)
44 nfv 1398 . . . 4 z(y 𝜔 → χ)
45 eleq1 2078 . . . . . 6 (x = y → (x 𝜔 ↔ y 𝜔))
4645biimprd 147 . . . . 5 (x = y → (y 𝜔 → x 𝜔))
47 bj-findis.1 . . . . 5 (x = y → (φχ))
4846, 47imim12d 68 . . . 4 (x = y → ((x 𝜔 → φ) → (y 𝜔 → χ)))
49 eleq1 2078 . . . . . 6 (x = z → (x 𝜔 ↔ z 𝜔))
5049biimpd 132 . . . . 5 (x = z → (x 𝜔 → z 𝜔))
51 eqtr 2035 . . . . . . . 8 ((x = z z = ∅) → x = ∅)
52 bj-findis.0 . . . . . . . 8 (x = ∅ → (ψφ))
5351, 52syl 14 . . . . . . 7 ((x = z z = ∅) → (ψφ))
5453expimpd 345 . . . . . 6 (x = z → ((z = ∅ ψ) → φ))
55 eqtr 2035 . . . . . . . . 9 ((x = z z = suc y) → x = suc y)
56 bj-findis.suc . . . . . . . . 9 (x = suc y → (θφ))
5755, 56syl 14 . . . . . . . 8 ((x = z z = suc y) → (θφ))
5857expimpd 345 . . . . . . 7 (x = z → ((z = suc y θ) → φ))
5958rexlimdvw 2410 . . . . . 6 (x = z → (y 𝜔 (z = suc y θ) → φ))
6054, 59jaod 624 . . . . 5 (x = z → (((z = ∅ ψ) y 𝜔 (z = suc y θ)) → φ))
6150, 60imim12d 68 . . . 4 (x = z → ((z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ))) → (x 𝜔 → φ)))
6231, 42, 43, 44, 48, 61setindis 7381 . . 3 (z(y z (y 𝜔 → χ) → (z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))) → x(x 𝜔 → φ))
6328, 62syl 14 . 2 ((ψ y 𝜔 (χθ)) → x(x 𝜔 → φ))
64 df-ral 2285 . 2 (x 𝜔 φx(x 𝜔 → φ))
6563, 64sylibr 137 1 ((ψ y 𝜔 (χθ)) → x 𝜔 φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 616  wal 1224   = wceq 1226  wnf 1325   wcel 1370  wral 2280  wrex 2281  c0 3197  suc csuc 4047  𝜔com 4236
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-in1 532  ax-in2 533  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-13 1381  ax-14 1382  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000  ax-nul 3853  ax-pr 3914  ax-un 4116  ax-setind 4200  ax-bd0 7232  ax-bdim 7233  ax-bdan 7234  ax-bdor 7235  ax-bdn 7236  ax-bdal 7237  ax-bdex 7238  ax-bdeq 7239  ax-bdel 7240  ax-bdsb 7241  ax-bdsep 7303  ax-infvn 7359
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-fal 1232  df-nf 1326  df-sb 1624  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-dif 2893  df-un 2895  df-in 2897  df-ss 2904  df-nul 3198  df-sn 3352  df-pr 3353  df-uni 3551  df-int 3586  df-suc 4053  df-iom 4237  df-bdc 7260  df-bj-ind 7346
This theorem is referenced by:  bj-findisg  7394  bj-findes  7395
  Copyright terms: Public domain W3C validator