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

Metamath Proof Explorer

Theorem wemapso2

Description: An alternative to having a well-order on R in wemapso is to restrict the function set to finitely-supported functions. (Contributed by Mario Carneiro, 8-Feb-2015) (Revised by AV, 1-Jul-2019)

Ref Expression
Hypotheses wemapso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
wemapso2.u ⊢ 𝑈 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
Assertion wemapso2 ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or 𝑈 )

Proof

Step Hyp Ref Expression
1 wemapso.t ⊢ 𝑇 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ∈ 𝐴 ( ( 𝑥 ‘ 𝑧 ) 𝑆 ( 𝑦 ‘ 𝑧 ) ∧ ∀ 𝑤 ∈ 𝐴 ( 𝑤 𝑅 𝑧 → ( 𝑥 ‘ 𝑤 ) = ( 𝑦 ‘ 𝑤 ) ) ) }
2 wemapso2.u ⊢ 𝑈 = { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 }
3 1 2 wemapso2lem ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) ∧ 𝑍 ∈ V ) → 𝑇 Or 𝑈 )
4 3 expcom ⊢ ( 𝑍 ∈ V → ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or 𝑈 ) )
5 so0 ⊢ 𝑇 Or ∅
6 relfsupp ⊢ Rel finSupp
7 6 brrelex2i ⊢ ( 𝑥 finSupp 𝑍 → 𝑍 ∈ V )
8 7 con3i ⊢ ( ¬ 𝑍 ∈ V → ¬ 𝑥 finSupp 𝑍 )
9 8 ralrimivw ⊢ ( ¬ 𝑍 ∈ V → ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
10 rabeq0 ⊢ ( { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ ↔ ∀ 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ¬ 𝑥 finSupp 𝑍 )
11 9 10 sylibr ⊢ ( ¬ 𝑍 ∈ V → { 𝑥 ∈ ( 𝐵 ↑m 𝐴 ) ∣ 𝑥 finSupp 𝑍 } = ∅ )
12 2 11 eqtrid ⊢ ( ¬ 𝑍 ∈ V → 𝑈 = ∅ )
13 soeq2 ⊢ ( 𝑈 = ∅ → ( 𝑇 Or 𝑈 ↔ 𝑇 Or ∅ ) )
14 12 13 syl ⊢ ( ¬ 𝑍 ∈ V → ( 𝑇 Or 𝑈 ↔ 𝑇 Or ∅ ) )
15 5 14 mpbiri ⊢ ( ¬ 𝑍 ∈ V → 𝑇 Or 𝑈 )
16 15 a1d ⊢ ( ¬ 𝑍 ∈ V → ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or 𝑈 ) )
17 4 16 pm2.61i ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝑅 Or 𝐴 ∧ 𝑆 Or 𝐵 ) → 𝑇 Or 𝑈 )