Metamath Proof Explorer

Theorem madeval2

Description: Alternative characterization of the made by function. (Contributed by Scott Fenton, 17-Dec-2021)

Ref Expression
Assertion madeval2 ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )

Proof

Step Hyp Ref Expression
1 madeval ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) )
2 scutcl ⊢ ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) ∈ No )
3 eleq1 ⊢ ( ( 𝑎 |s 𝑏 ) = 𝑥 → ( ( 𝑎 |s 𝑏 ) ∈ No ↔ 𝑥 ∈ No ) )
4 3 biimpd ⊢ ( ( 𝑎 |s 𝑏 ) = 𝑥 → ( ( 𝑎 |s 𝑏 ) ∈ No → 𝑥 ∈ No ) )
5 2 4 mpan9 ⊢ ( ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → 𝑥 ∈ No )
6 5 rexlimivw ⊢ ( ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → 𝑥 ∈ No )
7 6 rexlimivw ⊢ ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) → 𝑥 ∈ No )
8 7 pm4.71ri ⊢ ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ↔ ( 𝑥 ∈ No ∧ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) )
9 8 abbii ⊢ { 𝑥 ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ No ∧ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) }
10 eleq1 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑦 ∈ <<s ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ) )
11 breq1 ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑦 |s 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
12 10 11 anbi12d ⊢ ( 𝑦 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) ) )
13 12 rexxp ⊢ ( ∃ 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) ↔ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
14 imaindm ⊢ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) = ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ dom |s ) )
15 dmscut ⊢ dom |s = <<s
16 15 ineq2i ⊢ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ dom |s ) = ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s )
17 16 imaeq2i ⊢ ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ dom |s ) ) = ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) )
18 14 17 eqtri ⊢ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) = ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) )
19 18 eleq2i ⊢ ( 𝑥 ∈ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) ↔ 𝑥 ∈ ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) ) )
20 vex ⊢ 𝑥 ∈ V
21 20 elima ⊢ ( 𝑥 ∈ ( |s “ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) ) ↔ ∃ 𝑦 ∈ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) 𝑦 |s 𝑥 )
22 elin ⊢ ( 𝑦 ∈ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) ↔ ( 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∧ 𝑦 ∈ <<s ) )
23 22 anbi1i ⊢ ( ( 𝑦 ∈ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) ∧ 𝑦 |s 𝑥 ) ↔ ( ( 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥 ) )
24 anass ⊢ ( ( ( 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥 ) ↔ ( 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∧ ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) ) )
25 23 24 bitri ⊢ ( ( 𝑦 ∈ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) ∧ 𝑦 |s 𝑥 ) ↔ ( 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∧ ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) ) )
26 25 rexbii2 ⊢ ( ∃ 𝑦 ∈ ( ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ∩ <<s ) 𝑦 |s 𝑥 ↔ ∃ 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) )
27 19 21 26 3bitri ⊢ ( 𝑥 ∈ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) ↔ ∃ 𝑦 ∈ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ( 𝑦 ∈ <<s ∧ 𝑦 |s 𝑥 ) )
28 df-br ⊢ ( 𝑎 <<s 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
29 28 anbi1i ⊢ ( ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) )
30 df-ov ⊢ ( 𝑎 |s 𝑏 ) = ( |s ‘ ⟨ 𝑎 , 𝑏 ⟩ )
31 30 eqeq1i ⊢ ( ( 𝑎 |s 𝑏 ) = 𝑥 ↔ ( |s ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑥 )
32 scutf ⊢ |s : <<s ⟶ No
33 ffn ⊢ ( |s : <<s ⟶ No → |s Fn <<s )
34 32 33 ax-mp ⊢ |s Fn <<s
35 fnbrfvb ⊢ ( ( |s Fn <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ) → ( ( |s ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
36 34 35 mpan ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s → ( ( |s ‘ ⟨ 𝑎 , 𝑏 ⟩ ) = 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
37 31 36 syl5bb ⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s → ( ( 𝑎 |s 𝑏 ) = 𝑥 ↔ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
38 37 pm5.32i ⊢ ( ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
39 29 38 bitri ⊢ ( ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
40 39 2rexbii ⊢ ( ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ↔ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ∧ ⟨ 𝑎 , 𝑏 ⟩ |s 𝑥 ) )
41 13 27 40 3bitr4i ⊢ ( 𝑥 ∈ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) ↔ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) )
42 41 abbi2i ⊢ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) = { 𝑥 ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) }
43 df-rab ⊢ { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } = { 𝑥 ∣ ( 𝑥 ∈ No ∧ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) ) }
44 9 42 43 3eqtr4i ⊢ ( |s “ ( 𝒫 ∪ ( M “ 𝐴 ) × 𝒫 ∪ ( M “ 𝐴 ) ) ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) }
45 1 44 eqtrdi ⊢ ( 𝐴 ∈ On → ( M ‘ 𝐴 ) = { 𝑥 ∈ No ∣ ∃ 𝑎 ∈ 𝒫 ∪ ( M “ 𝐴 ) ∃ 𝑏 ∈ 𝒫 ∪ ( M “ 𝐴 ) ( 𝑎 <<s 𝑏 ∧ ( 𝑎 |s 𝑏 ) = 𝑥 ) } )