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 simp2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 )
28 fex2 ⊢ ( ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ⟶ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ∈ V ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V )
29 19 26 27 28 syl3anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V )
30 19 ffnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) Fn ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )
31 dffn4 ⊢ ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) Fn ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
32 30 31 sylib ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
33 n0 ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 )
34 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 )
35 nfixp1 ⊢ Ⅎ 𝑥 X 𝑥 ∈ 𝐴 𝐵
36 35 nfel2 ⊢ Ⅎ 𝑥 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵
37 nfv ⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 )
38 35 37 nfrex ⊢ Ⅎ 𝑥 ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 )
39 simplrr ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → 𝑧 ∈ 𝐵 )
40 iftrue ⊢ ( 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) = 𝑧 )
41 csbeq1a ⊢ ( 𝑥 = 𝑘 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
42 41 equcoms ⊢ ( 𝑘 = 𝑥 → 𝐵 = ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
43 42 eqcomd ⊢ ( 𝑘 = 𝑥 → ⦋ 𝑘 / 𝑥 ⦌ 𝐵 = 𝐵 )
44 40 43 eleq12d ⊢ ( 𝑘 = 𝑥 → ( if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ 𝑧 ∈ 𝐵 ) )
45 39 44 syl5ibrcom ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
46 vex ⊢ 𝑔 ∈ V
47 46 elixp ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑔 Fn 𝐴 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ) )
48 47 simprbi ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
49 48 adantr ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 )
50 nfv ⊢ Ⅎ 𝑘 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵
51 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
52 51 nfel2 ⊢ Ⅎ 𝑥 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵
53 fveq2 ⊢ ( 𝑥 = 𝑘 → ( 𝑔 ‘ 𝑥 ) = ( 𝑔 ‘ 𝑘 ) )
54 53 41 eleq12d ⊢ ( 𝑥 = 𝑘 → ( ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
55 50 52 54 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
56 49 55 sylib ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐴 ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
57 56 r19.21bi ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
58 iffalse ⊢ ( ¬ 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) = ( 𝑔 ‘ 𝑘 ) )
59 58 eleq1d ⊢ ( ¬ 𝑘 = 𝑥 → ( if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ( 𝑔 ‘ 𝑘 ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
60 57 59 syl5ibrcom ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → ( ¬ 𝑘 = 𝑥 → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
61 45 60 pm2.61d ⊢ ( ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) ∧ 𝑘 ∈ 𝐴 ) → if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
62 61 ralrimiva ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
63 ixpfn ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → 𝑔 Fn 𝐴 )
64 63 adantr ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑔 Fn 𝐴 )
65 64 fndmd ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → dom 𝑔 = 𝐴 )
66 46 dmex ⊢ dom 𝑔 ∈ V
67 65 66 eqeltrrdi ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝐴 ∈ V )
68 mptelixpg ⊢ ( 𝐴 ∈ V → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
69 67 68 syl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ↔ ∀ 𝑘 ∈ 𝐴 if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ∈ ⦋ 𝑘 / 𝑥 ⦌ 𝐵 ) )
70 62 69 mpbird ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵 )
71 nfcv ⊢ Ⅎ 𝑘 𝐵
72 71 51 41 cbvixp ⊢ X 𝑥 ∈ 𝐴 𝐵 = X 𝑘 ∈ 𝐴 ⦋ 𝑘 / 𝑥 ⦌ 𝐵
73 70 72 eleqtrrdi ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑥 ∈ 𝐴 𝐵 )
74 simprl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
75 eqid ⊢ ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) )
76 vex ⊢ 𝑧 ∈ V
77 40 75 76 fvmpt ⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) = 𝑧 )
78 77 ad2antrl ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) = 𝑧 )
79 78 eqcomd ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) )
80 fveq1 ⊢ ( 𝑓 = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) → ( 𝑓 ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) )
81 80 eqeq2d ⊢ ( 𝑓 = ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) → ( 𝑧 = ( 𝑓 ‘ 𝑦 ) ↔ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) ) )
82 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) )
83 82 eqeq2d ⊢ ( 𝑦 = 𝑥 → ( 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑦 ) ↔ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) ) )
84 81 83 rspc2ev ⊢ ( ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = ( ( 𝑘 ∈ 𝐴 ↦ if ( 𝑘 = 𝑥 , 𝑧 , ( 𝑔 ‘ 𝑘 ) ) ) ‘ 𝑥 ) ) → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) )
85 73 74 79 84 syl3anc ⊢ ( ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) ) → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) )
86 85 exp32 ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑥 ∈ 𝐴 → ( 𝑧 ∈ 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) ) )
87 36 38 86 rexlimd ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( ∃ 𝑥 ∈ 𝐴 𝑧 ∈ 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
88 34 87 syl5bi ⊢ ( 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
89 88 exlimiv ⊢ ( ∃ 𝑔 𝑔 ∈ X 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
90 33 89 sylbi ⊢ ( X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
91 90 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
92 91 alrimiv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
93 ssab ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) } ↔ ∀ 𝑧 ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) ) )
94 92 93 sylibr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) } )
95 17 rnmpo ⊢ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) = { 𝑧 ∣ ∃ 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 ∃ 𝑦 ∈ 𝐴 𝑧 = ( 𝑓 ‘ 𝑦 ) }
96 94 95 sseqtrrdi ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ⊆ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
97 19 frnd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ⊆ ∪ 𝑥 ∈ 𝐴 𝐵 )
98 96 97 eqssd ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 = ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) )
99 foeq3 ⊢ ( ∪ 𝑥 ∈ 𝐴 𝐵 = ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) → ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ) )
100 98 99 syl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ran ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ) )
101 32 100 mpbird ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 )
102 fowdom ⊢ ( ( ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) ∈ V ∧ ( 𝑓 ∈ X 𝑥 ∈ 𝐴 𝐵 , 𝑦 ∈ 𝐴 ↦ ( 𝑓 ‘ 𝑦 ) ) : ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) –onto→ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )
103 29 101 102 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑊 ∧ X 𝑥 ∈ 𝐴 𝐵 ≠ ∅ ) → ∪ 𝑥 ∈ 𝐴 𝐵 ≼* ( X 𝑥 ∈ 𝐴 𝐵 × 𝐴 ) )