Metamath Proof Explorer

Theorem suppeqfsuppbi

Description: If two functions have the same support, one function is finitely supported iff the other one is finitely supported. (Contributed by AV, 30-Jun-2019)

Ref Expression
Assertion suppeqfsuppbi ( ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) → ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 simprlr ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) → Fun 𝐹 )
2 simprll ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) → 𝐹 ∈ 𝑈 )
3 simpl ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) → 𝑍 ∈ V )
4 funisfsupp ⊢ ( ( Fun 𝐹 ∧ 𝐹 ∈ 𝑈 ∧ 𝑍 ∈ V ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
5 1 2 3 4 syl3anc ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
6 5 adantr ⊢ ( ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) ∧ ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) ) → ( 𝐹 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
7 simpr ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) → Fun 𝐺 )
8 7 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ 𝑍 ∈ V ) → Fun 𝐺 )
9 simpl ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) → 𝐺 ∈ 𝑉 )
10 9 adantr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ 𝑍 ∈ V ) → 𝐺 ∈ 𝑉 )
11 simpr ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ 𝑍 ∈ V ) → 𝑍 ∈ V )
12 funisfsupp ⊢ ( ( Fun 𝐺 ∧ 𝐺 ∈ 𝑉 ∧ 𝑍 ∈ V ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
13 8 10 11 12 syl3anc ⊢ ( ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ∧ 𝑍 ∈ V ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
14 13 ex ⊢ ( ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) → ( 𝑍 ∈ V → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) ) )
15 14 adantl ⊢ ( ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) → ( 𝑍 ∈ V → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) ) )
16 15 impcom ⊢ ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
17 eleq1 ⊢ ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( ( 𝐹 supp 𝑍 ) ∈ Fin ↔ ( 𝐺 supp 𝑍 ) ∈ Fin ) )
18 17 bicomd ⊢ ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( ( 𝐺 supp 𝑍 ) ∈ Fin ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
19 16 18 sylan9bb ⊢ ( ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) ∧ ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) ) → ( 𝐺 finSupp 𝑍 ↔ ( 𝐹 supp 𝑍 ) ∈ Fin ) )
20 6 19 bitr4d ⊢ ( ( ( 𝑍 ∈ V ∧ ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) ) ∧ ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) ) → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) )
21 20 exp31 ⊢ ( 𝑍 ∈ V → ( ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) → ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) ) ) )
22 relfsupp ⊢ Rel finSupp
23 22 brrelex2i ⊢ ( 𝐹 finSupp 𝑍 → 𝑍 ∈ V )
24 22 brrelex2i ⊢ ( 𝐺 finSupp 𝑍 → 𝑍 ∈ V )
25 23 24 pm5.21ni ⊢ ( ¬ 𝑍 ∈ V → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) )
26 25 2a1d ⊢ ( ¬ 𝑍 ∈ V → ( ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) → ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) ) ) )
27 21 26 pm2.61i ⊢ ( ( ( 𝐹 ∈ 𝑈 ∧ Fun 𝐹 ) ∧ ( 𝐺 ∈ 𝑉 ∧ Fun 𝐺 ) ) → ( ( 𝐹 supp 𝑍 ) = ( 𝐺 supp 𝑍 ) → ( 𝐹 finSupp 𝑍 ↔ 𝐺 finSupp 𝑍 ) ) )