Metamath Proof Explorer


Theorem onfrALTlem5VD

Description: Virtual deduction proof of onfrALTlem5 . The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. onfrALTlem5 is onfrALTlem5VD without virtual deductions and was automatically derived from onfrALTlem5VD .

1:: |- a e.V
2:1: |- ( a i^i x ) e. V
3:2: |- ( [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) = (/) )
4:3: |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> -. ( a i^i x ) = (/) )
5:: |- ( ( a i^i x ) =/= (/) <-> -. ( a i^i x ) = (/) )
6:4,5: |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> ( a i^i x ) =/= (/) )
7:2: |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
8:: |- ( b =/= (/) <-> -. b = (/) )
9:8: |- A. b ( b =/= (/) <-> -. b = (/) )
10:2,9: |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> [. ( a i^i x ) / b ]. -. b = (/) )
11:7,10: |- ( -. [. ( a i^i x ) / b ]. b = (/) <-> [. ( a i^i x ) / b ]. b =/= (/) )
12:6,11: |- ( [. ( a i^i x ) / b ]. b =/= (/) <-> ( a i^i x ) =/= (/) )
13:2: |- ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) <-> ( a i^i x ) C_ ( a i^i x ) )
14:12,13: |- ( ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
15:2: |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( [. ( a i^i x ) / b ]. b C_ ( a i^i x ) /\ [. ( a i^i x ) / b ]. b =/= (/) ) )
16:15,14: |- ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) <-> ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) )
17:2: |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y )
18:2: |- [_ ( a i^i x ) / b ]_ b = ( a i^i x )
19:2: |- [_ ( a i^i x ) / b ]_ y = y
20:18,19: |- ( [_ ( a i^i x ) / b ]_ b i^i [_ ( a i^i x ) / b ]_ y ) = ( ( a i^i x ) i^i y )
21:17,20: |- [_ ( a i^i x ) / b ]_ ( b i^i y ) = ( ( a i^i x ) i^i y )
22:2: |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) )
23:2: |- [_ ( a i^i x ) / b ]_ (/) = (/)
24:21,23: |- ( [_ ( a i^i x ) / b ]_ ( b i^i y ) = [_ ( a i^i x ) / b ]_ (/) <-> ( ( a i^i x ) i^i y ) = (/) )
25:22,24: |- ( [. ( a i^i x ) / b ]. ( b i^i y ) = (/) <-> ( ( a i^i x ) i^i y ) = (/) )
26:2: |- ( [. ( a i^i x ) / b ]. y e. b <-> y e. ( a i^i x ) )
27:25,26: |- ( ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
28:2: |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. y e. b /\ [. ( a i^i x ) / b ]. ( b i^i y ) = (/) ) )
29:27,28: |- ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
30:29: |- A. y ( [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
31:30: |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
32:: |- ( E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) <-> E. y ( y e. ( a i^i x ) /\ ( ( a i^i x ) i^i y ) = (/) ) )
33:31,32: |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
34:2: |- ( E. y [. ( a i^i x ) / b ]. ( y e. b /\ ( b i^i y ) = (/) ) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
35:33,34: |- ( [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
36:: |- ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
37:36: |- A. b ( E. y e. b ( b i^i y ) = (/) <-> E. y ( y e. b /\ ( b i^i y ) = (/) ) )
38:2,37: |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> [. ( a i^i x ) / b ]. E. y ( y e. b /\ ( b i^i y ) = (/) ) )
39:35,38: |- ( [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) <-> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) )
40:16,39: |- ( ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
41:2: |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( [. ( a i^i x ) / b ]. ( b C_ ( a i^i x ) /\ b =/= (/) ) -> [. ( a i^i x ) / b ]. E. y e. b ( b i^i y ) = (/) ) )
qed:40,41: |- ( [. ( a i^i x ) / b ]. ( ( b C_ ( a i^i x ) /\ b =/= (/) ) -> E. y e. b ( b i^i y ) = (/) ) <-> ( ( ( a i^i x ) C_ ( a i^i x ) /\ ( a i^i x ) =/= (/) ) -> E. y e. ( a i^i x ) ( ( a i^i x ) i^i y ) = (/) ) )
(Contributed by Alan Sare, 22-Jul-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion onfrALTlem5VD [˙ax/b]˙baxbybby=axaxaxyaxaxy=

Proof

Step Hyp Ref Expression
1 vex aV
2 1 inex1 axV
3 sbcimg axV[˙ax/b]˙baxbybby=[˙ax/b]˙baxb[˙ax/b]˙ybby=
4 2 3 e0a [˙ax/b]˙baxbybby=[˙ax/b]˙baxb[˙ax/b]˙ybby=
5 sbcan [˙ax/b]˙baxb[˙ax/b]˙bax[˙ax/b]˙b
6 sseq1 b=axbaxaxax
7 2 6 sbcie [˙ax/b]˙baxaxax
8 df-ne b¬b=
9 8 sbcbii [˙ax/b]˙b[˙ax/b]˙¬b=
10 sbcng axV[˙ax/b]˙¬b=¬[˙ax/b]˙b=
11 10 bicomd axV¬[˙ax/b]˙b=[˙ax/b]˙¬b=
12 2 11 e0a ¬[˙ax/b]˙b=[˙ax/b]˙¬b=
13 eqsbc1 axV[˙ax/b]˙b=ax=
14 2 13 e0a [˙ax/b]˙b=ax=
15 14 necon3bbii ¬[˙ax/b]˙b=ax
16 9 12 15 3bitr2i [˙ax/b]˙bax
17 7 16 anbi12i [˙ax/b]˙bax[˙ax/b]˙baxaxax
18 5 17 bitri [˙ax/b]˙baxbaxaxax
19 df-rex ybby=yybby=
20 19 sbcbii [˙ax/b]˙ybby=[˙ax/b]˙yybby=
21 sbcan [˙ax/b]˙ybby=[˙ax/b]˙yb[˙ax/b]˙by=
22 sbcel2gv axV[˙ax/b]˙ybyax
23 2 22 e0a [˙ax/b]˙ybyax
24 sbceqg axV[˙ax/b]˙by=ax/bby=ax/b
25 2 24 e0a [˙ax/b]˙by=ax/bby=ax/b
26 csbin ax/bby=ax/bbax/by
27 csbvarg axVax/bb=ax
28 2 27 e0a ax/bb=ax
29 csbconstg axVax/by=y
30 2 29 e0a ax/by=y
31 28 30 ineq12i ax/bbax/by=axy
32 26 31 eqtri ax/bby=axy
33 csb0 ax/b=
34 32 33 eqeq12i ax/bby=ax/baxy=
35 25 34 bitri [˙ax/b]˙by=axy=
36 23 35 anbi12i [˙ax/b]˙yb[˙ax/b]˙by=yaxaxy=
37 21 36 bitri [˙ax/b]˙ybby=yaxaxy=
38 37 exbii y[˙ax/b]˙ybby=yyaxaxy=
39 sbcex2 [˙ax/b]˙yybby=y[˙ax/b]˙ybby=
40 df-rex yaxaxy=yyaxaxy=
41 38 39 40 3bitr4i [˙ax/b]˙yybby=yaxaxy=
42 20 41 bitri [˙ax/b]˙ybby=yaxaxy=
43 18 42 imbi12i [˙ax/b]˙baxb[˙ax/b]˙ybby=axaxaxyaxaxy=
44 4 43 bitri [˙ax/b]˙baxbybby=axaxaxyaxaxy=