Theorem madeval2 33285

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

Assertion

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

Distinct variable group:   𝑥,𝐴,𝑎,𝑏

Proof of Theorem madeval2

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		madeval 33284	. 2 ⊢ (𝐴 ∈ On → ( M ‘𝐴) = ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))))
2		scutcut 33261	. . . . . . . . 9 ⊢ (𝑎 <<s 𝑏 → ((𝑎 |s 𝑏) ∈ No ∧ 𝑎 <<s {(𝑎 |s 𝑏)} ∧ {(𝑎 |s 𝑏)} <<s 𝑏))
3	2	simp1d 1138	. . . . . . . 8 ⊢ (𝑎 <<s 𝑏 → (𝑎 |s 𝑏) ∈ No )
4		eleq1 2900	. . . . . . . . 9 ⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No ↔ 𝑥 ∈ No ))
5	4	biimpd 231	. . . . . . . 8 ⊢ ((𝑎 |s 𝑏) = 𝑥 → ((𝑎 |s 𝑏) ∈ No → 𝑥 ∈ No ))
6	3, 5	mpan9 509	. . . . . . 7 ⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No )
7	6	rexlimivw 3282	. . . . . 6 ⊢ (∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No )
8	7	rexlimivw 3282	. . . . 5 ⊢ (∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) → 𝑥 ∈ No )
9	8	pm4.71ri 563	. . . 4 ⊢ (∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (𝑥 ∈ No ∧ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)))
10	9	abbii 2886	. . 3 ⊢ {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No ∧ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))}
11		eleq1 2900	. . . . . . 7 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 ∈ <<s ↔ ⟨𝑎, 𝑏⟩ ∈ <<s ))
12		breq1 5062	. . . . . . 7 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → (𝑦 |s 𝑥 ↔ ⟨𝑎, 𝑏⟩ |s 𝑥))
13	11, 12	anbi12d 632	. . . . . 6 ⊢ (𝑦 = ⟨𝑎, 𝑏⟩ → ((𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ (⟨𝑎, 𝑏⟩ ∈ <<s ∧ ⟨𝑎, 𝑏⟩ |s 𝑥)))
14	13	rexxp 5708	. . . . 5 ⊢ (∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(⟨𝑎, 𝑏⟩ ∈ <<s ∧ ⟨𝑎, 𝑏⟩ |s 𝑥))
15		imaindm 33017	. . . . . . . 8 ⊢ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s ))
16		dmscut 33267	. . . . . . . . . 10 ⊢ dom |s = <<s
17	16	ineq2i 4186	. . . . . . . . 9 ⊢ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s ) = ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )
18	17	imaeq2i 5922	. . . . . . . 8 ⊢ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ dom |s )) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ))
19	15, 18	eqtri 2844	. . . . . . 7 ⊢ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ))
20	19	eleq2i 2904	. . . . . 6 ⊢ (𝑥 ∈ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ 𝑥 ∈ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )))
21		vex 3498	. . . . . . 7 ⊢ 𝑥 ∈ V
22	21	elima 5929	. . . . . 6 ⊢ (𝑥 ∈ ( |s “ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )) ↔ ∃𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥)
23		elin 4169	. . . . . . . . 9 ⊢ (𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ))
24	23	anbi1i 625	. . . . . . . 8 ⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ ((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥))
25		anass 471	. . . . . . . 8 ⊢ (((𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ 𝑦 ∈ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)))
26	24, 25	bitri 277	. . . . . . 7 ⊢ ((𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s ) ∧ 𝑦 |s 𝑥) ↔ (𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∧ (𝑦 ∈ <<s ∧ 𝑦 |s 𝑥)))
27	26	rexbii2 3245	. . . . . 6 ⊢ (∃𝑦 ∈ ((𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴)) ∩ <<s )𝑦 |s 𝑥 ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))
28	20, 22, 27	3bitri 299	. . . . 5 ⊢ (𝑥 ∈ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑦 ∈ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))(𝑦 ∈ <<s ∧ 𝑦 |s 𝑥))
29		df-br 5060	. . . . . . . 8 ⊢ (𝑎 <<s 𝑏 ↔ ⟨𝑎, 𝑏⟩ ∈ <<s )
30	29	anbi1i 625	. . . . . . 7 ⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (⟨𝑎, 𝑏⟩ ∈ <<s ∧ (𝑎 |s 𝑏) = 𝑥))
31		df-ov 7153	. . . . . . . . . 10 ⊢ (𝑎 |s 𝑏) = ( |s ‘⟨𝑎, 𝑏⟩)
32	31	eqeq1i 2826	. . . . . . . . 9 ⊢ ((𝑎 |s 𝑏) = 𝑥 ↔ ( |s ‘⟨𝑎, 𝑏⟩) = 𝑥)
33		scutf 33268	. . . . . . . . . . 11 ⊢ |s : <<s ⟶ No
34		ffn 6509	. . . . . . . . . . 11 ⊢ ( |s : <<s ⟶ No → |s Fn <<s )
35	33, 34	ax-mp 5	. . . . . . . . . 10 ⊢ |s Fn <<s
36		fnbrfvb 6713	. . . . . . . . . 10 ⊢ (( |s Fn <<s ∧ ⟨𝑎, 𝑏⟩ ∈ <<s ) → (( |s ‘⟨𝑎, 𝑏⟩) = 𝑥 ↔ ⟨𝑎, 𝑏⟩ |s 𝑥))
37	35, 36	mpan 688	. . . . . . . . 9 ⊢ (⟨𝑎, 𝑏⟩ ∈ <<s → (( |s ‘⟨𝑎, 𝑏⟩) = 𝑥 ↔ ⟨𝑎, 𝑏⟩ |s 𝑥))
38	32, 37	syl5bb 285	. . . . . . . 8 ⊢ (⟨𝑎, 𝑏⟩ ∈ <<s → ((𝑎 |s 𝑏) = 𝑥 ↔ ⟨𝑎, 𝑏⟩ |s 𝑥))
39	38	pm5.32i 577	. . . . . . 7 ⊢ ((⟨𝑎, 𝑏⟩ ∈ <<s ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (⟨𝑎, 𝑏⟩ ∈ <<s ∧ ⟨𝑎, 𝑏⟩ |s 𝑥))
40	30, 39	bitri 277	. . . . . 6 ⊢ ((𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ (⟨𝑎, 𝑏⟩ ∈ <<s ∧ ⟨𝑎, 𝑏⟩ |s 𝑥))
41	40	2rexbii 3248	. . . . 5 ⊢ (∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(⟨𝑎, 𝑏⟩ ∈ <<s ∧ ⟨𝑎, 𝑏⟩ |s 𝑥))
42	14, 28, 41	3bitr4i 305	. . . 4 ⊢ (𝑥 ∈ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) ↔ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))
43	42	abbi2i 2953	. . 3 ⊢ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}
44		df-rab 3147	. . 3 ⊢ {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)} = {𝑥 ∣ (𝑥 ∈ No ∧ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥))}
45	10, 43, 44	3eqtr4i 2854	. 2 ⊢ ( |s “ (𝒫 ∪ ( M “ 𝐴) × 𝒫 ∪ ( M “ 𝐴))) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)}
46	1, 45	syl6eq 2872	1 ⊢ (𝐴 ∈ On → ( M ‘𝐴) = {𝑥 ∈ No ∣ ∃𝑎 ∈ 𝒫 ∪ ( M “ 𝐴)∃𝑏 ∈ 𝒫 ∪ ( M “ 𝐴)(𝑎 <<s 𝑏 ∧ (𝑎 |s 𝑏) = 𝑥)})

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1533   ∈ wcel 2110  {cab 2799  ∃wrex 3139  {crab 3142   ∩ cin 3935  𝒫 cpw 4539  {csn 4561  ⟨cop 4567  ∪ cuni 4832   class class class wbr 5059   × cxp 5548  dom cdm 5550   “ cima 5553  Oncon0 6186   Fn wfn 6345  ⟶wf 6346  ‘cfv 6350  (class class class)co 7150   No csur 33142   <<s csslt 33245   |s cscut 33247   M cmade 33274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793  ax-rep 5183  ax-sep 5196  ax-nul 5203  ax-pow 5259  ax-pr 5322  ax-un 7455

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rmo 3146  df-rab 3147  df-v 3497  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4562  df-pr 4564  df-tp 4566  df-op 4568  df-uni 4833  df-int 4870  df-iun 4914  df-br 5060  df-opab 5122  df-mpt 5140  df-tr 5166  df-id 5455  df-eprel 5460  df-po 5469  df-so 5470  df-fr 5509  df-we 5511  df-xp 5556  df-rel 5557  df-cnv 5558  df-co 5559  df-dm 5560  df-rn 5561  df-res 5562  df-ima 5563  df-pred 6143  df-ord 6189  df-on 6190  df-suc 6192  df-iota 6309  df-fun 6352  df-fn 6353  df-f 6354  df-f1 6355  df-fo 6356  df-f1o 6357  df-fv 6358  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-wrecs 7941  df-recs 8002  df-1o 8096  df-2o 8097  df-no 33145  df-slt 33146  df-bday 33147  df-sslt 33246  df-scut 33248  df-made 33279

This theorem is referenced by: (None)