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

Metamath Proof Explorer

Theorem sspred

Description: Another subset/predecessor class relationship. (Contributed by Scott Fenton, 6-Feb-2011)

Ref Expression
Assertion sspred ( ( 𝐵 ⊆ 𝐴 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )

Proof

Step Hyp Ref Expression
1 sseqin2 ⊢ ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∩ 𝐵 ) = 𝐵 )
2 df-pred ⊢ Pred ( 𝑅 , 𝐴 , 𝑋 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
3 2 sseq1i ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ↔ ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐵 )
4 dfss2 ⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
5 in32 ⊢ ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
6 5 eqeq1i ⊢ ( ( ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ∩ 𝐵 ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
7 3 4 6 3bitri ⊢ ( Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
8 ineq1 ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
9 8 eqeq1d ⊢ ( ( 𝐴 ∩ 𝐵 ) = 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ↔ ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) )
10 9 biimpa ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) )
11 df-pred ⊢ Pred ( 𝑅 , 𝐵 , 𝑋 ) = ( 𝐵 ∩ ( ◡ 𝑅 “ { 𝑋 } ) )
12 10 11 2 3eqtr4g ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → Pred ( 𝑅 , 𝐵 , 𝑋 ) = Pred ( 𝑅 , 𝐴 , 𝑋 ) )
13 12 eqcomd ⊢ ( ( ( 𝐴 ∩ 𝐵 ) = 𝐵 ∧ ( ( 𝐴 ∩ 𝐵 ) ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) = ( 𝐴 ∩ ( ◡ 𝑅 “ { 𝑋 } ) ) ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )
14 1 7 13 syl2anb ⊢ ( ( 𝐵 ⊆ 𝐴 ∧ Pred ( 𝑅 , 𝐴 , 𝑋 ) ⊆ 𝐵 ) → Pred ( 𝑅 , 𝐴 , 𝑋 ) = Pred ( 𝑅 , 𝐵 , 𝑋 ) )