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

Metamath Proof Explorer

Theorem isowe2

Description: A weak form of isowe that does not need Replacement. (Contributed by Mario Carneiro, 18-Nov-2014)

Ref Expression
Assertion isowe2 ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )

Proof

Step Hyp Ref Expression
1 simpl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) )
2 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐻 “ 𝑥 ) = ( 𝐻 “ 𝑦 ) )
3 2 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝐻 “ 𝑥 ) ∈ V ↔ ( 𝐻 “ 𝑦 ) ∈ V ) )
4 3 spvv ⊢ ( ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V → ( 𝐻 “ 𝑦 ) ∈ V )
5 4 adantl ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( 𝐻 “ 𝑦 ) ∈ V )
6 1 5 isofrlem ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( 𝑆 Fr 𝐵 → 𝑅 Fr 𝐴 ) )
7 isosolem ⊢ ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) → ( 𝑆 Or 𝐵 → 𝑅 Or 𝐴 ) )
8 7 adantr ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( 𝑆 Or 𝐵 → 𝑅 Or 𝐴 ) )
9 6 8 anim12d ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( ( 𝑆 Fr 𝐵 ∧ 𝑆 Or 𝐵 ) → ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) ) )
10 df-we ⊢ ( 𝑆 We 𝐵 ↔ ( 𝑆 Fr 𝐵 ∧ 𝑆 Or 𝐵 ) )
11 df-we ⊢ ( 𝑅 We 𝐴 ↔ ( 𝑅 Fr 𝐴 ∧ 𝑅 Or 𝐴 ) )
12 9 10 11 3imtr4g ⊢ ( ( 𝐻 Isom 𝑅 , 𝑆 ( 𝐴 , 𝐵 ) ∧ ∀ 𝑥 ( 𝐻 “ 𝑥 ) ∈ V ) → ( 𝑆 We 𝐵 → 𝑅 We 𝐴 ) )