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

Proof

Step Hyp Ref Expression
1 vex ${⊢}{a}\in \mathrm{V}$
2 1 inex1 ${⊢}{a}\cap {x}\in \mathrm{V}$
3 sbcimg
4 2 3 e0a
5 sbcan
6 sseq1 ${⊢}{b}={a}\cap {x}\to \left({b}\subseteq {a}\cap {x}↔{a}\cap {x}\subseteq {a}\cap {x}\right)$
7 2 6 sbcie
8 df-ne ${⊢}{b}\ne \varnothing ↔¬{b}=\varnothing$
9 8 sbcbii
10 sbcng
11 10 bicomd
12 2 11 e0a
13 eqsbc3
14 2 13 e0a
15 14 necon3bbii
16 9 12 15 3bitr2i
17 7 16 anbi12i
18 5 17 bitri
19 df-rex ${⊢}\exists {y}\in {b}\phantom{\rule{.4em}{0ex}}{b}\cap {y}=\varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {b}\wedge {b}\cap {y}=\varnothing \right)$
20 19 sbcbii
21 sbcan
22 sbcel2gv
23 2 22 e0a
24 sbceqg
25 2 24 e0a
26 csbin
27 csbvarg
28 2 27 e0a
29 csbconstg
30 2 29 e0a
31 28 30 ineq12i
32 26 31 eqtri
33 csb0
34 32 33 eqeq12i
35 25 34 bitri
36 23 35 anbi12i
37 21 36 bitri
38 37 exbii
39 sbcex2
40 df-rex ${⊢}\exists {y}\in \left({a}\cap {x}\right)\phantom{\rule{.4em}{0ex}}\left({a}\cap {x}\right)\cap {y}=\varnothing ↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({y}\in \left({a}\cap {x}\right)\wedge \left({a}\cap {x}\right)\cap {y}=\varnothing \right)$
41 38 39 40 3bitr4i
42 20 41 bitri
43 18 42 imbi12i
44 4 43 bitri