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 𝑈 )