Metamath Proof Explorer

Theorem impprop

Description: The implication between two sentences of propositional calculus is a sentence of propositional calculus. (Contributed by Thomas van Maaren, 21-Aug-2026)

Ref Expression
Assertion impprop 
|- ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. PROP )

Proof

Step Hyp Ref Expression
1 df-prop 
 |-  PROP = setrecs ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) )
2 prex 
 |-  { x , y } e. _V
3 2 a1i 
 |-  ( ( x e. PROP /\ y e. PROP ) -> { x , y } e. _V )
4 prssi 
 |-  ( ( x e. PROP /\ y e. PROP ) -> { x , y } C_ PROP )
5 1 3 4 setrec1 
 |-  ( ( x e. PROP /\ y e. PROP ) -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) C_ PROP )
6 vex 
 |-  y e. _V
7 vex 
 |-  x e. _V
8 oveq2 
 |-  ( v = y -> ( u prop-> v ) = ( u prop-> y ) )
9 8 eqeq2d 
 |-  ( v = y -> ( z = ( u prop-> v ) <-> z = ( u prop-> y ) ) )
10 oveq1 
 |-  ( u = x -> ( u prop-> y ) = ( x prop-> y ) )
11 10 eqeq2d 
 |-  ( u = x -> ( z = ( u prop-> y ) <-> z = ( x prop-> y ) ) )
12 6 7 9 11 ceqsex2v 
 |-  ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> z = ( x prop-> y ) )
13 12 bilanri 
 |-  ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) )
14 3anass 
 |-  ( ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) )
15 14 exbii 
 |-  ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) )
16 19.42v 
 |-  ( E. u ( v = y /\ ( u = x /\ z = ( u prop-> v ) ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) )
17 15 16 bitri 
 |-  ( E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) )
18 17 exbii 
 |-  ( E. v E. u ( v = y /\ u = x /\ z = ( u prop-> v ) ) <-> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) )
19 13 18 sylib 
 |-  ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) )
20 olc 
 |-  ( v = y -> ( v = x \/ v = y ) )
21 vex 
 |-  v e. _V
22 21 elpr 
 |-  ( v e. { x , y } <-> ( v = x \/ v = y ) )
23 20 22 sylibr 
 |-  ( v = y -> v e. { x , y } )
24 orc 
 |-  ( u = x -> ( u = x \/ u = y ) )
25 vex 
 |-  u e. _V
26 25 elpr 
 |-  ( u e. { x , y } <-> ( u = x \/ u = y ) )
27 24 26 sylibr 
 |-  ( u = x -> u e. { x , y } )
28 27 anim1i 
 |-  ( ( u = x /\ z = ( u prop-> v ) ) -> ( u e. { x , y } /\ z = ( u prop-> v ) ) )
29 28 eximi 
 |-  ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) )
30 df-rex 
 |-  ( E. u e. { x , y } z = ( u prop-> v ) <-> E. u ( u e. { x , y } /\ z = ( u prop-> v ) ) )
31 29 30 sylibr 
 |-  ( E. u ( u = x /\ z = ( u prop-> v ) ) -> E. u e. { x , y } z = ( u prop-> v ) )
32 31 olcd 
 |-  ( E. u ( u = x /\ z = ( u prop-> v ) ) -> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) )
33 23 32 anim12i 
 |-  ( ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
34 33 eximi 
 |-  ( E. v ( v = y /\ E. u ( u = x /\ z = ( u prop-> v ) ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
35 19 34 syl 
 |-  ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
36 df-rex 
 |-  ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) <-> E. v ( v e. { x , y } /\ ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
37 35 36 sylibr 
 |-  ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) )
38 37 orcd 
 |-  ( ( ( x e. PROP /\ y e. PROP ) /\ z = ( x prop-> y ) ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) )
39 38 ex 
 |-  ( ( x e. PROP /\ y e. PROP ) -> ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) )
40 39 alrimiv 
 |-  ( ( x e. PROP /\ y e. PROP ) -> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) )
41 ovex 
 |-  ( x prop-> y ) e. _V
42 elab6g 
 |-  ( ( x prop-> y ) e. _V -> ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) ) )
43 41 42 ax-mp 
 |-  ( ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } <-> A. z ( z = ( x prop-> y ) -> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) )
44 40 43 sylibr 
 |-  ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } )
45 rexeq 
 |-  ( w = { x , y } -> ( E. u e. w z = ( u prop-> v ) <-> E. u e. { x , y } z = ( u prop-> v ) ) )
46 45 orbi2d 
 |-  ( w = { x , y } -> ( ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
47 46 rexeqbi1dv 
 |-  ( w = { x , y } -> ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) <-> E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) ) )
48 47 orbi1d 
 |-  ( w = { x , y } -> ( ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) <-> ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) ) )
49 48 abbidv 
 |-  ( w = { x , y } -> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } )
50 eqid 
 |-  ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) = ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } )
51 2 dfproplem 
 |-  { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } e. _V
52 49 50 51 fvmpt 
 |-  ( { x , y } e. _V -> ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } )
53 2 52 ax-mp 
 |-  ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) = { z | ( E. v e. { x , y } ( z = ( prop-. ` v ) \/ E. u e. { x , y } z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) }
54 44 53 eleqtrrdi 
 |-  ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. ( ( w e. _V |-> { z | ( E. v e. w ( z = ( prop-. ` v ) \/ E. u e. w z = ( u prop-> v ) ) \/ E. n e. NN z = ( propvar ` n ) ) } ) ` { x , y } ) )
55 5 54 sseldd 
 |-  ( ( x e. PROP /\ y e. PROP ) -> ( x prop-> y ) e. PROP )