Metamath Proof Explorer

Theorem sbcoreleleqVD

Description: Virtual deduction proof of sbcoreleleq . The following user's proof is completed by invoking mmj2's unify command and using mmj2's StepSelector to pick all remaining steps of the Metamath proof.

1:: |- (. A e. B ->. A e. B ).
2:1,?: e1a |- (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
3:1,?: e1a |- (. A e. B ->. ( [. A / y ]. y e. x <-> A e. x ) ).
4:1,?: e1a |- (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
5:2,3,4,?: e111 |- (. A e. B ->. ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
6:1,?: e1a |- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
7:5,6: e11 |- (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ).
qed:7: |- ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )
(Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sbcoreleleqVD 
|- ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )

Proof

Step Hyp Ref Expression
1 sbcor 
 |-  ( [. A / y ]. ( ( x e. y \/ y e. x ) \/ x = y ) <-> ( [. A / y ]. ( x e. y \/ y e. x ) \/ [. A / y ]. x = y ) )
2 1 a1i 
 |-  ( A e. B -> ( [. A / y ]. ( ( x e. y \/ y e. x ) \/ x = y ) <-> ( [. A / y ]. ( x e. y \/ y e. x ) \/ [. A / y ]. x = y ) ) )
3 df-3or 
 |-  ( ( x e. y \/ y e. x \/ x = y ) <-> ( ( x e. y \/ y e. x ) \/ x = y ) )
4 3 bicomi 
 |-  ( ( ( x e. y \/ y e. x ) \/ x = y ) <-> ( x e. y \/ y e. x \/ x = y ) )
5 4 sbcbii 
 |-  ( [. A / y ]. ( ( x e. y \/ y e. x ) \/ x = y ) <-> [. A / y ]. ( x e. y \/ y e. x \/ x = y ) )
6 5 a1i 
 |-  ( A e. B -> ( [. A / y ]. ( ( x e. y \/ y e. x ) \/ x = y ) <-> [. A / y ]. ( x e. y \/ y e. x \/ x = y ) ) )
7 sbcor 
 |-  ( [. A / y ]. ( x e. y \/ y e. x ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x ) )
8 7 a1i 
 |-  ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x ) ) )
9 8 orbi1d 
 |-  ( A e. B -> ( ( [. A / y ]. ( x e. y \/ y e. x ) \/ [. A / y ]. x = y ) <-> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x ) \/ [. A / y ]. x = y ) ) )
10 2 6 9 3bitr3d 
 |-  ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x ) \/ [. A / y ]. x = y ) ) )
11 df-3or 
 |-  ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) <-> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x ) \/ [. A / y ]. x = y ) )
12 10 11 bitr4di 
 |-  ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) )
13 12 dfvd1ir 
 |-  (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
14 sbcel2gv 
 |-  ( A e. B -> ( [. A / y ]. x e. y <-> x e. A ) )
15 14 dfvd1ir 
 |-  (. A e. B ->. ( [. A / y ]. x e. y <-> x e. A ) ).
16 sbcel1v 
 |-  ( [. A / y ]. y e. x <-> A e. x )
17 eqsbc2 
 |-  ( A e. B -> ( [. A / y ]. x = y <-> x = A ) )
18 17 dfvd1ir 
 |-  (. A e. B ->. ( [. A / y ]. x = y <-> x = A ) ).
19 3orbi123 
 |-  ( ( ( [. A / y ]. x e. y <-> x e. A ) /\ ( [. A / y ]. y e. x <-> A e. x ) /\ ( [. A / y ]. x = y <-> x = A ) ) -> ( ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )
20 19 3impexpbicomi 
 |-  ( ( [. A / y ]. x e. y <-> x e. A ) -> ( ( [. A / y ]. y e. x <-> A e. x ) -> ( ( [. A / y ]. x = y <-> x = A ) -> ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ) ) )
21 15 16 18 20 e101 
 |-  (. A e. B ->. ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ).
22 biantr 
 |-  ( ( ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) /\ ( ( x e. A \/ A e. x \/ x = A ) <-> ( [. A / y ]. x e. y \/ [. A / y ]. y e. x \/ [. A / y ]. x = y ) ) ) -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )
23 13 21 22 e11an 
 |-  (. A e. B ->. ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) ).
24 23 in1 
 |-  ( A e. B -> ( [. A / y ]. ( x e. y \/ y e. x \/ x = y ) <-> ( x e. A \/ A e. x \/ x = A ) ) )