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

Metamath Proof Explorer

Theorem ixpiunwdom

Description: Describe an onto function from the indexed cartesian product to the indexed union. Together with ixpssmapg this shows that U_ x e. A B and X_ x e. A B have closely linked cardinalities. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion ixpiunwdom ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑓 ∈ V
2 1 elixp ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 ) )
3 2 simprbi ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 )
4 ssiun2 ⊢ ( 𝑥 ∈ 𝐴 → 𝐵 ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
5 4 sseld ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
6 5 ralimia ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
7 3 6 syl ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
8 nfv ⊢ Ⅎ 𝑦 ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵
9 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
10 9 nfel2 ⊢ Ⅎ 𝑥 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵
11 fveq2 ⊢ ( 𝑥 = 𝑦 → ( 𝑓 ‘ 𝑥 ) = ( 𝑓 ‘ 𝑦 ) )
12 11 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
13 8 10 12 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑓 ‘ 𝑥 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
14 7 13 sylib ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) ∧ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
16 15 ralrimiva ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∀ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
17 eqid ⊢ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) = ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) )
18 17 fmpo ⊢ ( ∀ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∀ 𝑦 ∈ 𝐴 ( 𝑓 ‘ 𝑦 ) ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
19 16 18 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 )
20 ixpssmap2g ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
21 20 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) )
22 ovex ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) ∈ V
23 22 ssex ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ⊆ ( ∪ 𝑥 ∈ 𝐴 𝐵 ↑m 𝐴 ) → X 𝑥 ∈ 𝐴 𝐵 ∈ V )
24 21 23 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → X 𝑥 ∈ 𝐴 𝐵 ∈ V )
25 simp1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → 𝐴 ∈ 𝑉 )
26 24 25 xpexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ∈ V )
27 19 26 fexd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V )
28 19 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) Fn ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )
29 dffn4 ⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) Fn ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
30 28 29 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
31 n0 ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 )
32 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
33 nfixp1 ⊢ Ⅎ 𝑥 X 𝑥 ∈ 𝐴 𝐵
34 33 nfel2 ⊢ Ⅎ 𝑥 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵
35 nfv ⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 )
36 33 35 nfrexw ⊢ Ⅎ 𝑥 ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 )
37 simplrr ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
38 iftrue ⊢ ( 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) = 𝑧 )
39 csbeq1a ⊢ ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
40 39 equcoms ⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
41 40 eqcomd ⊢ ( 𝑘 = 𝑥 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 )
42 38 41 eleq12d ⊢ ( 𝑘 = 𝑥 → ( if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
43 37 42 syl5ibrcom ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
44 vex ⊢ 𝑔 ∈ V
45 44 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )
46 45 simprbi ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
47 46 adantr ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
48 nfv ⊢ Ⅎ 𝑘 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵
49 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
50 49 nfel2 ⊢ Ⅎ 𝑥 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵
51 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑘 ) )
52 51 39 eleq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
53 48 50 52 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
54 47 53 sylib ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
55 54 r19.21bi ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
56 iffalse ⊢ ( ¬ 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) = ( 𝑔 ‘ 𝑘 ) )
57 56 eleq1d ⊢ ( ¬ 𝑘 = 𝑥 → ( if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
58 55 57 syl5ibrcom ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
59 43 58 pm2.61d ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
60 59 ralrimiva ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
61 ixpfn ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑔 Fn 𝐴 )
62 61 adantr ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑔 Fn 𝐴 )
63 62 fndmd ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → dom 𝑔 = 𝐴 )
64 44 dmex ⊢ dom 𝑔 ∈ V
65 63 64 eqeltrrdi ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 ∈ V )
66 mptelixpg ⊢ ( 𝐴 ∈ V → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
67 65 66 syl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
68 60 67 mpbird ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
69 nfcv ⊢ Ⅎ 𝑘 𝐵
70 69 49 39 cbvixp ⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
71 68 70 eleqtrrdi ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑥 ∈ 𝐴 𝐵 )
72 simprl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
73 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) )
74 vex ⊢ 𝑧 ∈ V
75 38 73 74 fvmpt ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) = 𝑧 )
76 75 ad2antrl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) = 𝑧 )
77 76 eqcomd ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) )
78 fveq1 ⊢ ( 𝑓 = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) )
79 78 eqeq2d ⊢ ( 𝑓 = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) → ( 𝑧 = ( 𝑓 ‘ 𝑦 ) ↔ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) ) )
80 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) )
81 80 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) ↔ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) ) )
82 79 81 rspc2ev ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) ) → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) )
83 71 72 77 82 syl3anc ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) )
84 83 exp32 ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) ) )
85 34 36 84 rexlimd ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
86 32 85 biimtrid ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
87 86 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
88 31 87 sylbi ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
89 88 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
90 89 alrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
91 ssab ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) } ↔ ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
92 90 91 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) } )
93 17 rnmpo ⊢ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) }
94 92 93 sseqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
95 19 frnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
96 94 95 eqssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
97 foeq3 ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ) )
98 96 97 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ) )
99 30 98 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 )
100 fowdom ⊢ ( ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V ∧ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )
101 27 99 100 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )