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 bilani ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ∃ 𝑗 ∈ 𝐴 𝑥 ∈ 𝐵 )
66 24 27 63 65 r19.29af2 ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
67 66 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
68 14 67 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
69 vex ⊢ 𝑥 ∈ V
70 33 69 opth ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ ↔ ( ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) ∧ 𝑥 = 𝑦 ) )
71 70 simprbi ⊢ ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 )
72 71 rgen2w ⊢ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 )
73 72 a1i ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) )
74 68 73 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) ) )
75 eqid ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
76 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑦 ) )
77 id ⊢ ( 𝑥 = 𝑦 → 𝑥 = 𝑦 )
78 76 77 opeq12d ⊢ ( 𝑥 = 𝑦 → ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ )
79 75 78 f1mpt ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ = ⟨ ( 𝑔 ‘ 𝑦 ) , 𝑦 ⟩ → 𝑥 = 𝑦 ) ) )
80 74 79 sylibr ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
81 opex ⊢ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ V
82 75 fvmpt2 ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ∈ V ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
83 81 82 mpan2 ⊢ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
84 37 83 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) = ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
85 84 fveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = ( 2nd ‘ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) )
86 33 69 op2nd ⊢ ( 2nd ‘ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) = 𝑥
87 85 86 eqtrdi ⊢ ( ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) ∧ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ) → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 )
88 87 ex ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
89 14 88 ralrimi ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 )
90 80 89 jca ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
91 nfcv ⊢ Ⅎ 𝑗 𝑘
92 91 3 nfel ⊢ Ⅎ 𝑗 𝑘 ∈ 𝐴
93 15 92 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑘 ∈ 𝐴 )
94 nfcv ⊢ Ⅎ 𝑗 𝑊
95 54 94 nfel ⊢ Ⅎ 𝑗 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊
96 93 95 nfim ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
97 eleq1w ⊢ ( 𝑗 = 𝑘 → ( 𝑗 ∈ 𝐴 ↔ 𝑘 ∈ 𝐴 ) )
98 97 anbi2d ⊢ ( 𝑗 = 𝑘 → ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ↔ ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) ) )
99 58 eleq1d ⊢ ( 𝑗 = 𝑘 → ( 𝐵 ∈ 𝑊 ↔ ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) )
100 98 99 imbi12d ⊢ ( 𝑗 = 𝑘 → ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) ) )
101 96 100 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
102 101 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 )
103 nfcv ⊢ Ⅎ 𝑘 𝐵
104 3 51 103 54 58 cbviunf ⊢ ∪ 𝑗 ∈ 𝐴 𝐵 = ∪ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵
105 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) → ∪ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ V )
106 104 105 eqeltrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑗 ⦌ 𝐵 ∈ 𝑊 ) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
107 1 102 106 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V )
108 mptexg ⊢ ( ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V → ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ∈ V )
109 f1eq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) )
110 nfcv ⊢ Ⅎ 𝑥 𝑓
111 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
112 110 111 nfeq ⊢ Ⅎ 𝑥 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ )
113 fveq1 ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( 𝑓 ‘ 𝑥 ) = ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) )
114 113 fveqeq2d ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ↔ ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
115 112 114 ralbid ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ↔ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) )
116 109 115 anbi12d ⊢ ( 𝑓 = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) → ( ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ↔ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) ) )
117 116 spcegv ⊢ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ∈ V → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
118 107 108 117 3syl ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
119 118 adantr ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ( ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↦ ⟨ ( 𝑔 ‘ 𝑥 ) , 𝑥 ⟩ ) ‘ 𝑥 ) ) = 𝑥 ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) ) )
120 90 119 mpd ⊢ ( ( 𝜑 ∧ ( 𝑔 : ∪ 𝑗 ∈ 𝐴 𝐵 ⟶ 𝐴 ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 𝑥 ∈ ⦋ ( 𝑔 ‘ 𝑥 ) / 𝑗 ⦌ 𝐵 ) ) → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )
121 9 120 exlimddv ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑗 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∧ ∀ 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑥 ) ) = 𝑥 ) )