Metamath Proof Explorer

Theorem suppovss

Description: A bound for the support of an operation. (Contributed by Thierry Arnoux, 19-Jul-2023)

Ref Expression
Hypotheses suppovss.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
suppovss.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
suppovss.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
suppovss.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
suppovss.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐷 )
suppovss.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
Assertion suppovss ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) )

Proof

Step Hyp Ref Expression
1 suppovss.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2 suppovss.g ⊢ 𝐺 = ( 𝑥 ∈ 𝐴 ↦ ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
3 suppovss.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 suppovss.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 )
5 suppovss.z ⊢ ( 𝜑 → 𝑍 ∈ 𝐷 )
6 suppovss.1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐶 ∈ 𝐷 )
7 6 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 )
8 1 fmpo ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝐷 ↔ 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 )
9 7 8 sylib ⊢ ( 𝜑 → 𝐹 : ( 𝐴 × 𝐵 ) ⟶ 𝐷 )
10 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
11 10 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
12 df-ov ⊢ ( 𝑥 𝐹 𝑦 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ )
13 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) )
14 13 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 ∈ 𝐴 )
15 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ 𝐵 )
16 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝜑 )
17 16 14 15 6 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 ∈ 𝐷 )
18 1 ovmpt4g ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ∧ 𝐶 ∈ 𝐷 ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
19 14 15 17 18 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
20 12 19 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐶 )
21 4 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
22 21 mptexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V )
23 22 2 fmptd ⊢ ( 𝜑 → 𝐺 : 𝐴 ⟶ V )
24 ssidd ⊢ ( 𝜑 → ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
25 snex ⊢ { 𝑍 } ∈ V
26 25 a1i ⊢ ( 𝜑 → { 𝑍 } ∈ V )
27 4 26 xpexd ⊢ ( 𝜑 → ( 𝐵 × { 𝑍 } ) ∈ V )
28 23 24 3 27 suppssr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( 𝐺 ‘ 𝑥 ) = ( 𝐵 × { 𝑍 } ) )
29 28 fveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑦 ) )
30 16 13 29 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝐵 × { 𝑍 } ) ‘ 𝑦 ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
32 2 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) ∈ V ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
33 31 22 32 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) = ( 𝑦 ∈ 𝐵 ↦ 𝐶 ) )
34 6 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → 𝐶 ∈ 𝐷 )
35 33 34 fvmpt2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝐶 )
36 16 14 15 35 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝐶 )
37 16 5 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑍 ∈ 𝐷 )
38 fvconst2g ⊢ ( ( 𝑍 ∈ 𝐷 ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐵 × { 𝑍 } ) ‘ 𝑦 ) = 𝑍 )
39 37 15 38 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐵 × { 𝑍 } ) ‘ 𝑦 ) = 𝑍 )
40 30 36 39 3eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 = 𝑍 )
41 11 20 40 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
42 41 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) ∧ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
43 elxp2 ⊢ ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ↔ ∃ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
44 43 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
45 42 44 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
46 45 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
47 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
48 47 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
49 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 ∈ 𝐴 )
50 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) )
51 50 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ 𝐵 )
52 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝜑 )
53 52 49 51 6 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 ∈ 𝐷 )
54 49 51 53 18 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
55 12 54 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐶 )
56 52 49 51 35 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝐶 )
57 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) ∈ V )
58 34 33 57 fmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) : 𝐵 ⟶ V )
59 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) )
60 59 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) )
61 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
62 61 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) = ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
63 62 cbviunv ⊢ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 )
64 60 63 sseqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
65 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝜑 )
66 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) )
67 66 eldifad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝑘 ∈ 𝐴 )
68 23 24 3 27 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) )
69 eleq1w ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
70 69 anbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
71 61 fneq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) Fn 𝐵 ↔ ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ) )
72 70 71 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) Fn 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ) ) )
73 58 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) Fn 𝐵 )
74 72 73 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑘 ) Fn 𝐵 )
75 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
76 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑍 ∈ 𝐷 )
77 fnsuppeq0 ⊢ ( ( ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑍 ∈ 𝐷 ) → ( ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ ↔ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) )
78 74 75 76 77 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ ↔ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) )
79 78 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) → ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
80 65 67 68 79 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
81 80 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
82 nfcv ⊢ Ⅎ 𝑘 ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
83 82 iunxdif3 ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
84 81 83 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
85 dfin4 ⊢ ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) )
86 suppssdm ⊢ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ dom 𝐺
87 86 23 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ 𝐴 )
88 sseqin2 ⊢ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
89 87 88 sylib ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
90 85 89 eqtr3id ⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
91 90 iuneq1d ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
92 84 91 eqtr3d ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
93 92 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
94 64 93 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
95 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑍 ∈ 𝐷 )
96 58 94 21 95 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑍 )
97 96 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑍 )
98 56 97 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 = 𝑍 )
99 48 55 98 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
100 99 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
101 elxp2 ⊢ ( 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
102 101 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
103 100 102 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
104 103 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
105 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) )
106 difxp ⊢ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) = ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) )
107 105 106 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → 𝑧 ∈ ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
108 elun ⊢ ( 𝑧 ∈ ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ↔ ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∨ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
109 107 108 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∨ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
110 46 104 109 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
111 9 110 suppss ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) )