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 ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 sbcor ⊢ ( [ 𝐴 / 𝑦 ] ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) ↔ ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) )
2 1 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) ↔ ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) )
3 df-3or ⊢ ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) )
4 3 bicomi ⊢ ( ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
5 4 sbcbii ⊢ ( [ 𝐴 / 𝑦 ] ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) ↔ [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) )
6 5 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ 𝑥 = 𝑦 ) ↔ [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ) )
7 sbcor ⊢ ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ) )
8 7 a1i ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ) ) )
9 8 orbi1d ⊢ ( 𝐴 ∈ 𝐵 → ( ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) )
10 2 6 9 3bitr3d ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) )
11 df-3or ⊢ ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ↔ ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ) ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) )
12 10 11 bitr4di ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) )
13 12 dfvd1ir ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) )    )
14 sbcel2gv ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) )
15 14 dfvd1ir ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 )    )
16 sbcel1v ⊢ ( [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 )
17 eqsbc2 ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) )
18 17 dfvd1ir ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 )    )
19 3orbi123 ⊢ ( ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) ∧ ( [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) ∧ ( [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) ) → ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ) )
20 19 3impexpbicomi ⊢ ( ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ 𝐴 ) → ( ( [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ↔ 𝐴 ∈ 𝑥 ) → ( ( [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ↔ 𝑥 = 𝐴 ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) ) ) )
21 15 16 18 20 e101 ⊢ (    𝐴 ∈ 𝐵    ▶    ( ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) )    )
22 biantr ⊢ ( ( ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) ∧ ( ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ↔ ( [ 𝐴 / 𝑦 ] 𝑥 ∈ 𝑦 ∨ [ 𝐴 / 𝑦 ] 𝑦 ∈ 𝑥 ∨ [ 𝐴 / 𝑦 ] 𝑥 = 𝑦 ) ) ) → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ) )
23 13 21 22 e11an ⊢ (    𝐴 ∈ 𝐵    ▶    ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) )    )
24 23 in1 ⊢ ( 𝐴 ∈ 𝐵 → ( [ 𝐴 / 𝑦 ] ( 𝑥 ∈ 𝑦 ∨ 𝑦 ∈ 𝑥 ∨ 𝑥 = 𝑦 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝐴 ∈ 𝑥 ∨ 𝑥 = 𝐴 ) ) )