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 biimpi ⊢ ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) → ∃ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
45 44 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ∃ 𝑥 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ∃ 𝑦 ∈ 𝐵 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
46 42 45 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
47 46 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
48 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
49 48 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
50 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑥 ∈ 𝐴 )
51 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) )
52 51 eldifad ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝑦 ∈ 𝐵 )
53 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝜑 )
54 53 50 52 6 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 ∈ 𝐷 )
55 50 52 54 18 syl3anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝑥 𝐹 𝑦 ) = 𝐶 )
56 12 55 eqtr3id ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝐶 )
57 53 50 52 35 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝐶 )
58 fvexd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) ∈ V )
59 34 33 58 fmpt2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) : 𝐵 ⟶ V )
60 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) )
61 60 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) )
62 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑘 ) )
63 62 oveq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) = ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
64 63 cbviunv ⊢ ∪ 𝑥 ∈ 𝐴 ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 )
65 61 64 sseqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
66 simpl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝜑 )
67 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) )
68 67 eldifad ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → 𝑘 ∈ 𝐴 )
69 23 24 3 27 suppssr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) )
70 eleq1w ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
71 70 anbi2d ⊢ ( 𝑥 = 𝑘 → ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
72 62 fneq1d ⊢ ( 𝑥 = 𝑘 → ( ( 𝐺 ‘ 𝑥 ) Fn 𝐵 ↔ ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ) )
73 71 72 imbi12d ⊢ ( 𝑥 = 𝑘 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) Fn 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ) ) )
74 59 ffnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑥 ) Fn 𝐵 )
75 73 74 chvarvv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( 𝐺 ‘ 𝑘 ) Fn 𝐵 )
76 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
77 5 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝑍 ∈ 𝐷 )
78 fnsuppeq0 ⊢ ( ( ( 𝐺 ‘ 𝑘 ) Fn 𝐵 ∧ 𝐵 ∈ 𝑊 ∧ 𝑍 ∈ 𝐷 ) → ( ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ ↔ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) )
79 75 76 77 78 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ( ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ ↔ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) )
80 79 biimpar ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ∧ ( 𝐺 ‘ 𝑘 ) = ( 𝐵 × { 𝑍 } ) ) → ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
81 66 68 69 80 syl21anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) → ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
82 81 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ )
83 nfcv ⊢ Ⅎ 𝑘 ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
84 83 iunxdif3 ⊢ ( ∀ 𝑘 ∈ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∅ → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
85 82 84 syl ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
86 dfin4 ⊢ ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) )
87 suppssdm ⊢ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ dom 𝐺
88 87 23 fssdm ⊢ ( 𝜑 → ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ 𝐴 )
89 sseqin2 ⊢ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ⊆ 𝐴 ↔ ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
90 88 89 sylib ⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
91 86 90 eqtr3id ⊢ ( 𝜑 → ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) = ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) )
92 91 iuneq1d ⊢ ( 𝜑 → ∪ 𝑘 ∈ ( 𝐴 ∖ ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
93 85 92 eqtr3d ⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
94 93 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∪ 𝑘 ∈ 𝐴 ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) = ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
95 65 94 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐺 ‘ 𝑥 ) supp 𝑍 ) ⊆ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) )
96 5 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑍 ∈ 𝐷 )
97 59 95 21 96 suppssr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑍 )
98 97 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( ( 𝐺 ‘ 𝑥 ) ‘ 𝑦 ) = 𝑍 )
99 57 98 eqtr3d ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → 𝐶 = 𝑍 )
100 49 56 99 3eqtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
101 100 adantl3r ⊢ ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ∧ 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
102 elxp2 ⊢ ( 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
103 102 biimpi ⊢ ( 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
104 103 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ )
105 101 104 r19.29vva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
106 105 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ∧ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
107 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) )
108 difxp ⊢ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) = ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) )
109 107 108 eleqtrdi ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → 𝑧 ∈ ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
110 elun ⊢ ( 𝑧 ∈ ( ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∪ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) ↔ ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∨ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
111 109 110 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝑧 ∈ ( ( 𝐴 ∖ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ) × 𝐵 ) ∨ 𝑧 ∈ ( 𝐴 × ( 𝐵 ∖ ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) )
112 47 106 111 mpjaodan ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐴 × 𝐵 ) ∖ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) ) ) → ( 𝐹 ‘ 𝑧 ) = 𝑍 )
113 9 112 suppss ⊢ ( 𝜑 → ( 𝐹 supp 𝑍 ) ⊆ ( ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) × ∪ 𝑘 ∈ ( 𝐺 supp ( 𝐵 × { 𝑍 } ) ) ( ( 𝐺 ‘ 𝑘 ) supp 𝑍 ) ) )