This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sseliALT

Description: Alternate proof of sseli illustrating the use of the weak deduction theorem to prove it from the inference sselii . (Contributed by NM, 24-Aug-2018) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis sseliALT.1 ⊢ 𝐴 ⊆ 𝐵
Assertion sseliALT ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 sseliALT.1 ⊢ 𝐴 ⊆ 𝐵
2 biidd ⊢ ( 𝐴 = if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) → ( 𝐶 ∈ 𝐵 ↔ 𝐶 ∈ 𝐵 ) )
3 eleq2 ⊢ ( 𝐵 = if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) → ( 𝐶 ∈ 𝐵 ↔ 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
4 eleq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) → ( 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ↔ if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) ∈ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
5 sseq1 ⊢ ( 𝐴 = if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) → ( 𝐴 ⊆ 𝐵 ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ 𝐵 ) )
6 sseq2 ⊢ ( 𝐵 = if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) → ( if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ 𝐵 ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
7 biidd ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) → ( if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
8 sseq1 ⊢ ( { ∅ } = if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) → ( { ∅ } ⊆ { ∅ } ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ { ∅ } ) )
9 sseq2 ⊢ ( { ∅ } = if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) → ( if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ { ∅ } ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
10 biidd ⊢ ( ∅ = if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) → ( if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ↔ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) ) )
11 ssid ⊢ { ∅ } ⊆ { ∅ }
12 5 6 7 8 9 10 1 11 keephyp3v ⊢ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ⊆ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } )
13 eleq2 ⊢ ( 𝐴 = if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) → ( 𝐶 ∈ 𝐴 ↔ 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
14 biidd ⊢ ( 𝐵 = if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) → ( 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ↔ 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
15 eleq1 ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) → ( 𝐶 ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ↔ if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
16 eleq2 ⊢ ( { ∅ } = if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) → ( ∅ ∈ { ∅ } ↔ ∅ ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
17 biidd ⊢ ( { ∅ } = if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } ) → ( ∅ ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ↔ ∅ ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
18 eleq1 ⊢ ( ∅ = if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) → ( ∅ ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ↔ if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } ) ) )
19 0ex ⊢ ∅ ∈ V
20 19 snid ⊢ ∅ ∈ { ∅ }
21 13 14 15 16 17 18 20 elimhyp3v ⊢ if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) ∈ if ( 𝐶 ∈ 𝐴 , 𝐴 , { ∅ } )
22 12 21 sselii ⊢ if ( 𝐶 ∈ 𝐴 , 𝐶 , ∅ ) ∈ if ( 𝐶 ∈ 𝐴 , 𝐵 , { ∅ } )
23 2 3 4 22 dedth3v ⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ 𝐵 )