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 9409
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 9381 for a bounded version not requiring ax-setind 4220. See finds 4266 for a proof in IZF. From this version, it is easy to prove of finds 4266, finds2 4267, finds1 4268. (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 9394 . . . . 5 (z 𝜔 ↔ (z = ∅ y 𝜔 z = suc y))
2 pm3.21 251 . . . . . . . 8 (ψ → (z = ∅ → (z = ∅ ψ)))
32ad2antrr 457 . . . . . . 7 (((ψ y 𝜔 (χθ)) y z (y 𝜔 → χ)) → (z = ∅ → (z = ∅ ψ)))
4 pm2.04 76 . . . . . . . . . . 11 ((y z → (y 𝜔 → χ)) → (y 𝜔 → (y zχ)))
54ralimi2 2375 . . . . . . . . . 10 (y z (y 𝜔 → χ) → y 𝜔 (y zχ))
6 imim2 49 . . . . . . . . . . . 12 ((χθ) → ((y zχ) → (y zθ)))
76ral2imi 2379 . . . . . . . . . . 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 2444 . . . . . . . . . . 11 ((y 𝜔 (y zθ) y 𝜔 z = suc y) → y 𝜔 ((y zθ) z = suc y))
11 vex 2554 . . . . . . . . . . . . . . . 16 y V
1211sucid 4120 . . . . . . . . . . . . . . 15 y suc y
13 eleq2 2098 . . . . . . . . . . . . . . 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 398 . . . . . . . . . . . . 13 (z = suc y → ((y zθ) → (z = suc y θ)))
1918impcom 116 . . . . . . . . . . . 12 (((y zθ) z = suc y) → (z = suc y θ))
2019reximi 2410 . . . . . . . . . . 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 445 . . . . . . 7 (((ψ y 𝜔 (χθ)) y z (y 𝜔 → χ)) → (y 𝜔 z = suc yy 𝜔 (z = suc y θ)))
253, 24orim12d 699 . . . . . 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 1751 . . 3 ((ψ y 𝜔 (χθ)) → z(y z (y 𝜔 → χ) → (z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))))
29 nfv 1418 . . . . 5 x y 𝜔
30 bj-findis.nf1 . . . . 5 xχ
3129, 30nfim 1461 . . . 4 x(y 𝜔 → χ)
32 nfv 1418 . . . . 5 x z 𝜔
33 nfv 1418 . . . . . . 7 x z = ∅
34 bj-findis.nf0 . . . . . . 7 xψ
3533, 34nfan 1454 . . . . . 6 x(z = ∅ ψ)
36 nfcv 2175 . . . . . . 7 x𝜔
37 nfv 1418 . . . . . . . 8 x z = suc y
38 bj-findis.nfsuc . . . . . . . 8 xθ
3937, 38nfan 1454 . . . . . . 7 x(z = suc y θ)
4036, 39nfrexxy 2355 . . . . . 6 xy 𝜔 (z = suc y θ)
4135, 40nfor 1463 . . . . 5 x((z = ∅ ψ) y 𝜔 (z = suc y θ))
4232, 41nfim 1461 . . . 4 x(z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))
43 nfv 1418 . . . 4 z(x 𝜔 → φ)
44 nfv 1418 . . . 4 z(y 𝜔 → χ)
45 eleq1 2097 . . . . . 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 2097 . . . . . 6 (x = z → (x 𝜔 ↔ z 𝜔))
5049biimpd 132 . . . . 5 (x = z → (x 𝜔 → z 𝜔))
51 eqtr 2054 . . . . . . . 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 2054 . . . . . . . . 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 2430 . . . . . 6 (x = z → (y 𝜔 (z = suc y θ) → φ))
6054, 59jaod 636 . . . . 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 9397 . . 3 (z(y z (y 𝜔 → χ) → (z 𝜔 → ((z = ∅ ψ) y 𝜔 (z = suc y θ)))) → x(x 𝜔 → φ))
6328, 62syl 14 . 2 ((ψ y 𝜔 (χθ)) → x(x 𝜔 → φ))
64 df-ral 2305 . 2 (x 𝜔 φx(x 𝜔 → φ))
6563, 64sylibr 137 1 ((ψ y 𝜔 (χθ)) → x 𝜔 φ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97   wo 628  wal 1240   = wceq 1242  wnf 1346   wcel 1390  wral 2300  wrex 2301  c0 3218  suc csuc 4068  𝜔com 4256
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 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-nul 3874  ax-pr 3935  ax-un 4136  ax-setind 4220  ax-bd0 9248  ax-bdim 9249  ax-bdan 9250  ax-bdor 9251  ax-bdn 9252  ax-bdal 9253  ax-bdex 9254  ax-bdeq 9255  ax-bdel 9256  ax-bdsb 9257  ax-bdsep 9319  ax-infvn 9375
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-fal 1248  df-nf 1347  df-sb 1643  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-rab 2309  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-nul 3219  df-sn 3373  df-pr 3374  df-uni 3572  df-int 3607  df-suc 4074  df-iom 4257  df-bdc 9276  df-bj-ind 9362
This theorem is referenced by:  bj-findisg  9410  bj-findes  9411
  Copyright terms: Public domain W3C validator