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

Metamath Proof Explorer

Theorem aciunf1lem

Description: Choice in an index union. (Contributed by Thierry Arnoux, 8-Nov-2019)

Ref Expression
Hypotheses acunirnmpt.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
acunirnmpt.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
aciunf1lem.a ⊢ Ⅎ 𝑗 𝐴
aciunf1lem.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
Assertion aciunf1lem ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )

Proof

Step Hyp Ref Expression
1 acunirnmpt.0 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 acunirnmpt.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ≠ ∅ )
3 aciunf1lem.a ⊢ Ⅎ 𝑗 𝐴
4 aciunf1lem.1 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 𝐵
6 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵
7 eqid ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑗 ∈ 𝐴 𝐵
8 csbeq1a ⊢ ( 𝑗 = ( 𝑔 ‘ 𝑥 ) → 𝐵 = ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
9 1 2 3 5 6 7 8 4 acunirnmpt2f ⊢ ( 𝜑 → ∃ 𝑔 ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
10 nfv ⊢ Ⅎ 𝑥 𝜑
11 nfv ⊢ Ⅎ 𝑥 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴
12 nfra1 ⊢ Ⅎ 𝑥 ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵
13 11 12 nfan ⊢ Ⅎ 𝑥 ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
14 10 13 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
15 nfv ⊢ Ⅎ 𝑗 𝜑
16 nfcv ⊢ Ⅎ 𝑗 𝑔
17 16 5 3 nff ⊢ Ⅎ 𝑗 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴
18 nfcv ⊢ Ⅎ 𝑗 𝑥
19 18 6 nfel ⊢ Ⅎ 𝑗 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵
20 5 19 nfralw ⊢ Ⅎ 𝑗 ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵
21 17 20 nfan ⊢ Ⅎ 𝑗 ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
22 15 21 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
23 18 5 nfel ⊢ Ⅎ 𝑗 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
24 22 23 nfan ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 )
25 nfcv ⊢ Ⅎ 𝑗 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩
26 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
27 25 26 nfel ⊢ Ⅎ 𝑗 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
28 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
29 28 simpld ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 )
30 29 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 )
31 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 )
32 30 31 ffvelcdmd ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑔 ‘ 𝑥 ) ∈ 𝐴 )
33 fvex ⊢ ( 𝑔 ‘ 𝑥 ) ∈ V
34 33 snid ⊢ ( 𝑔 ‘ 𝑥 ) ∈ { ( 𝑔 ‘ 𝑥 ) }
35 34 a1i ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑔 ‘ 𝑥 ) ∈ { ( 𝑔 ‘ 𝑥 ) } )
36 28 simprd ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
37 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 )
38 rsp ⊢ ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
39 36 37 38 sylc ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
40 39 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
41 35 40 jca ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑔 ‘ 𝑥 ) ∈ { ( 𝑔 ‘ 𝑥 ) } ∧ 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
42 opelxp ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { ( 𝑔 ‘ 𝑥 ) } × ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ↔ ( ( 𝑔 ‘ 𝑥 ) ∈ { ( 𝑔 ‘ 𝑥 ) } ∧ 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
43 41 42 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { ( 𝑔 ‘ 𝑥 ) } × ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
44 sneq ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → { 𝑘 } = { ( 𝑔 ‘ 𝑥 ) } )
45 csbeq1 ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 = ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 )
46 44 45 xpeq12d ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) = ( { ( 𝑔 ‘ 𝑥 ) } × ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) )
47 46 eleq2d ⊢ ( 𝑘 = ( 𝑔 ‘ 𝑥 ) → ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) ↔ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { ( 𝑔 ‘ 𝑥 ) } × ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) )
48 47 rspcev ⊢ ( ( ( 𝑔 ‘ 𝑥 ) ∈ 𝐴 ∧ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { ( 𝑔 ‘ 𝑥 ) } × ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∃ 𝑘 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) )
49 32 43 48 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑘 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) )
50 eliun ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑗 } × 𝐵 ) )
51 nfcv ⊢ Ⅎ 𝑘 𝐴
52 nfv ⊢ Ⅎ 𝑘 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑗 } × 𝐵 )
53 nfcv ⊢ Ⅎ 𝑗 { 𝑘 }
54 nfcsb1v ⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐵
55 53 54 nfxp ⊢ Ⅎ 𝑗 ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 )
56 25 55 nfel ⊢ Ⅎ 𝑗 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 )
57 sneq ⊢ ( 𝑗 = 𝑘 → { 𝑗 } = { 𝑘 } )
58 csbeq1a ⊢ ( 𝑗 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑗 ⦌ 𝐵 )
59 57 58 xpeq12d ⊢ ( 𝑗 = 𝑘 → ( { 𝑗 } × 𝐵 ) = ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) )
60 59 eleq2d ⊢ ( 𝑗 = 𝑘 → ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) ) )
61 3 51 52 56 60 cbvrexfw ⊢ ( ∃ 𝑗 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) )
62 50 61 bitri ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐴 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ( { 𝑘 } × ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ) )
63 49 62 sylibr ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑥 ∈ 𝐵 ) → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
64 eliun ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
65 64 biimpi ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
66 65 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
67 24 27 63 66 r19.29af2 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
68 67 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
69 14 68 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
70 vex ⊢ 𝑥 ∈ V
71 33 70 opth ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ ↔ ( ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) ∧ 𝑥 = 𝑦 ) )
72 71 simprbi ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 )
73 72 rgen2w ⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 )
74 73 a1i ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) )
75 69 74 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) ) )
76 eqid ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
77 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) )
78 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
79 77 78 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ )
80 76 79 f1mpt ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) ) )
81 75 80 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
82 opex ⊢ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ V
83 76 fvmpt2 ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ V ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
84 82 83 mpan2 ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
85 37 84 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
86 85 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = ( 2nd ‘ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) )
87 33 70 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) = 𝑥
88 86 87 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 )
89 88 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
90 14 89 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 )
91 81 90 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
92 nfcv ⊢ Ⅎ 𝑗 𝑘
93 92 3 nfel ⊢ Ⅎ 𝑗 𝑘 ∈ 𝐴
94 15 93 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝐴 )
95 nfcv ⊢ Ⅎ 𝑗 𝑊
96 54 95 nfel ⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊
97 94 96 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
98 eleq1w ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
99 98 anbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
100 58 eleq1d ⊢ ( 𝑗 = 𝑘 → ( 𝐵 ∈ 𝑊 ↔ ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) )
101 99 100 imbi12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) ) )
102 97 101 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
103 102 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
104 nfcv ⊢ Ⅎ 𝑘 𝐵
105 3 51 104 54 58 cbviunf ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵
106 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) → ∪ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ V )
107 105 106 eqeltrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
108 1 103 107 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
109 mptexg ⊢ ( ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ∈ V )
110 f1eq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
111 nfcv ⊢ Ⅎ 𝑥 𝑓
112 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
113 111 112 nfeq ⊢ Ⅎ 𝑥 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
114 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) )
115 114 fveqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ↔ ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
116 113 115 ralbid ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ↔ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
117 110 116 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ↔ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) ) )
118 117 spcegv ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ∈ V → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
119 108 109 118 3syl ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
120 119 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
121 91 120 mpd ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
122 9 121 exlimddv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )