r0weon

Description: A set-like well-ordering of the class of ordinal pairs. Proposition 7.58(1) of TakeutiZaring p. 54. (Contributed by Mario Carneiro, 7-Mar-2013) (Revised by Mario Carneiro, 26-Jun-2015)

	Ref	Expression
Hypotheses	leweon.1	⊢ 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) ) }
	r0weon.1	⊢ 𝑅 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∨ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) }
Assertion	r0weon	⊢ ( 𝑅 We ( On × On ) ∧ 𝑅 Se ( On × On ) )

Proof

Step	Hyp	Ref	Expression
1		leweon.1	⊢ 𝐿 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( On × On ) ∧ 𝑦 ∈ ( On × On ) ) ∧ ( ( 1^st ‘ 𝑥 ) ∈ ( 1^st ‘ 𝑦 ) ∨ ( ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑦 ) ∧ ( 2^nd ‘ 𝑥 ) ∈ ( 2^nd ‘ 𝑦 ) ) ) ) }
2		r0weon.1	⊢ 𝑅 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∨ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) }
3		fveq2	⊢ ( 𝑥 = 𝑧 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑧 ) )
4		fveq2	⊢ ( 𝑥 = 𝑧 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑧 ) )
5	3 4	uneq12d	⊢ ( 𝑥 = 𝑧 → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) )
6		eqid	⊢ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
7		fvex	⊢ ( 1^st ‘ 𝑧 ) ∈ V
8		fvex	⊢ ( 2^nd ‘ 𝑧 ) ∈ V
9	7 8	unex	⊢ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ V
10	5 6 9	fvmpt	⊢ ( 𝑧 ∈ ( On × On ) → ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) )
11		fveq2	⊢ ( 𝑥 = 𝑤 → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ 𝑤 ) )
12		fveq2	⊢ ( 𝑥 = 𝑤 → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ 𝑤 ) )
13	11 12	uneq12d	⊢ ( 𝑥 = 𝑤 → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
14		fvex	⊢ ( 1^st ‘ 𝑤 ) ∈ V
15		fvex	⊢ ( 2^nd ‘ 𝑤 ) ∈ V
16	14 15	unex	⊢ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∈ V
17	13 6 16	fvmpt	⊢ ( 𝑤 ∈ ( On × On ) → ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
18	10 17	breqan12d	⊢ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) → ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) E ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
19	16	epeli	⊢ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) E ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) )
20	18 19	bitrdi	⊢ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) → ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
21	10 17	eqeqan12d	⊢ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) → ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ↔ ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ) )
22	21	anbi1d	⊢ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) → ( ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∧ 𝑧 𝐿 𝑤 ) ↔ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) )
23	20 22	orbi12d	⊢ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) → ( ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∨ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∧ 𝑧 𝐿 𝑤 ) ) ↔ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∨ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) )
24	23	pm5.32i	⊢ ( ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∨ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∧ 𝑧 𝐿 𝑤 ) ) ) ↔ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∨ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) )
25	24	opabbii	⊢ { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∨ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∧ 𝑧 𝐿 𝑤 ) ) ) } = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) ∈ ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∨ ( ( ( 1^st ‘ 𝑧 ) ∪ ( 2^nd ‘ 𝑧 ) ) = ( ( 1^st ‘ 𝑤 ) ∪ ( 2^nd ‘ 𝑤 ) ) ∧ 𝑧 𝐿 𝑤 ) ) ) }
26	2 25	eqtr4i	⊢ 𝑅 = { ⟨ 𝑧 , 𝑤 ⟩ ∣ ( ( 𝑧 ∈ ( On × On ) ∧ 𝑤 ∈ ( On × On ) ) ∧ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) E ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∨ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑧 ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ‘ 𝑤 ) ∧ 𝑧 𝐿 𝑤 ) ) ) }
27		xp1st	⊢ ( 𝑥 ∈ ( On × On ) → ( 1^st ‘ 𝑥 ) ∈ On )
28		xp2nd	⊢ ( 𝑥 ∈ ( On × On ) → ( 2^nd ‘ 𝑥 ) ∈ On )
29		fvex	⊢ ( 1^st ‘ 𝑥 ) ∈ V
30	29	elon	⊢ ( ( 1^st ‘ 𝑥 ) ∈ On ↔ Ord ( 1^st ‘ 𝑥 ) )
31		fvex	⊢ ( 2^nd ‘ 𝑥 ) ∈ V
32	31	elon	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ On ↔ Ord ( 2^nd ‘ 𝑥 ) )
33		ordun	⊢ ( ( Ord ( 1^st ‘ 𝑥 ) ∧ Ord ( 2^nd ‘ 𝑥 ) ) → Ord ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
34	30 32 33	syl2anb	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ On ∧ ( 2^nd ‘ 𝑥 ) ∈ On ) → Ord ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
35	27 28 34	syl2anc	⊢ ( 𝑥 ∈ ( On × On ) → Ord ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
36	29 31	unex	⊢ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ V
37	36	elon	⊢ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ On ↔ Ord ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
38	35 37	sylibr	⊢ ( 𝑥 ∈ ( On × On ) → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ On )
39	6 38	fmpti	⊢ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) : ( On × On ) ⟶ On
40	39	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) : ( On × On ) ⟶ On )
41		epweon	⊢ E We On
42	41	a1i	⊢ ( ⊤ → E We On )
43	1	leweon	⊢ 𝐿 We ( On × On )
44	43	a1i	⊢ ( ⊤ → 𝐿 We ( On × On ) )
45		vex	⊢ 𝑢 ∈ V
46	45	dmex	⊢ dom 𝑢 ∈ V
47	45	rnex	⊢ ran 𝑢 ∈ V
48	46 47	unex	⊢ ( dom 𝑢 ∪ ran 𝑢 ) ∈ V
49		imadmres	⊢ ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ) = ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 )
50		inss2	⊢ ( 𝑢 ∩ ( On × On ) ) ⊆ ( On × On )
51		ssun1	⊢ dom 𝑢 ⊆ ( dom 𝑢 ∪ ran 𝑢 )
52		elinel2	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → 𝑥 ∈ ( On × On ) )
53		1st2nd2	⊢ ( 𝑥 ∈ ( On × On ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
54	52 53	syl	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
55		elinel1	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → 𝑥 ∈ 𝑢 )
56	54 55	eqeltrrd	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝑢 )
57	29 31	opeldm	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝑢 → ( 1^st ‘ 𝑥 ) ∈ dom 𝑢 )
58	56 57	syl	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 1^st ‘ 𝑥 ) ∈ dom 𝑢 )
59	51 58	sselid	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 1^st ‘ 𝑥 ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) )
60		ssun2	⊢ ran 𝑢 ⊆ ( dom 𝑢 ∪ ran 𝑢 )
61	29 31	opelrn	⊢ ( ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∈ 𝑢 → ( 2^nd ‘ 𝑥 ) ∈ ran 𝑢 )
62	56 61	syl	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 2^nd ‘ 𝑥 ) ∈ ran 𝑢 )
63	60 62	sselid	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 2^nd ‘ 𝑥 ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) )
64	59 63	prssd	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → { ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) } ⊆ ( dom 𝑢 ∪ ran 𝑢 ) )
65	52 27	syl	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 1^st ‘ 𝑥 ) ∈ On )
66	52 28	syl	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( 2^nd ‘ 𝑥 ) ∈ On )
67		ordunpr	⊢ ( ( ( 1^st ‘ 𝑥 ) ∈ On ∧ ( 2^nd ‘ 𝑥 ) ∈ On ) → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ { ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) } )
68	65 66 67	syl2anc	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ { ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) } )
69	64 68	sseldd	⊢ ( 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) )
70	69	rgen	⊢ ∀ 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 )
71		ssrab	⊢ ( ( 𝑢 ∩ ( On × On ) ) ⊆ { 𝑥 ∈ ( On × On ) ∣ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) } ↔ ( ( 𝑢 ∩ ( On × On ) ) ⊆ ( On × On ) ∧ ∀ 𝑥 ∈ ( 𝑢 ∩ ( On × On ) ) ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) ) )
72	50 70 71	mpbir2an	⊢ ( 𝑢 ∩ ( On × On ) ) ⊆ { 𝑥 ∈ ( On × On ) ∣ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) }
73		dmres	⊢ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) = ( 𝑢 ∩ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) )
74	39	fdmi	⊢ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) = ( On × On )
75	74	ineq2i	⊢ ( 𝑢 ∩ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ) = ( 𝑢 ∩ ( On × On ) )
76	73 75	eqtri	⊢ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) = ( 𝑢 ∩ ( On × On ) )
77	6	mptpreima	⊢ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ ( dom 𝑢 ∪ ran 𝑢 ) ) = { 𝑥 ∈ ( On × On ) ∣ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ ( dom 𝑢 ∪ ran 𝑢 ) }
78	72 76 77	3sstr4i	⊢ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ ( dom 𝑢 ∪ ran 𝑢 ) )
79		funmpt	⊢ Fun ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
80		resss	⊢ ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
81		dmss	⊢ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) → dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) )
82	80 81	ax-mp	⊢ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) )
83		funimass3	⊢ ( ( Fun ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ∧ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ dom ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ) → ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ) ⊆ ( dom 𝑢 ∪ ran 𝑢 ) ↔ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ ( dom 𝑢 ∪ ran 𝑢 ) ) ) )
84	79 82 83	mp2an	⊢ ( ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ) ⊆ ( dom 𝑢 ∪ ran 𝑢 ) ↔ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ⊆ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ ( dom 𝑢 ∪ ran 𝑢 ) ) )
85	78 84	mpbir	⊢ ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ dom ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) ↾ 𝑢 ) ) ⊆ ( dom 𝑢 ∪ ran 𝑢 )
86	49 85	eqsstrri	⊢ ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ⊆ ( dom 𝑢 ∪ ran 𝑢 )
87	48 86	ssexi	⊢ ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ∈ V
88	87	a1i	⊢ ( ⊤ → ( ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ∈ V )
89	26 40 42 44 88	fnwe	⊢ ( ⊤ → 𝑅 We ( On × On ) )
90		epse	⊢ E Se On
91	90	a1i	⊢ ( ⊤ → E Se On )
92		vuniex	⊢ ∪ 𝑢 ∈ V
93	92	pwex	⊢ 𝒫 ∪ 𝑢 ∈ V
94	93 93	xpex	⊢ ( 𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢 ) ∈ V
95	6	mptpreima	⊢ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) = { 𝑥 ∈ ( On × On ) ∣ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 }
96		df-rab	⊢ { 𝑥 ∈ ( On × On ) ∣ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 } = { 𝑥 ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) }
97	95 96	eqtri	⊢ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) = { 𝑥 ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) }
98	53	adantr	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ )
99		elssuni	⊢ ( ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ⊆ ∪ 𝑢 )
100	99	adantl	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ⊆ ∪ 𝑢 )
101	100	unssad	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( 1^st ‘ 𝑥 ) ⊆ ∪ 𝑢 )
102	29	elpw	⊢ ( ( 1^st ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ↔ ( 1^st ‘ 𝑥 ) ⊆ ∪ 𝑢 )
103	101 102	sylibr	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( 1^st ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 )
104	100	unssbd	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( 2^nd ‘ 𝑥 ) ⊆ ∪ 𝑢 )
105	31	elpw	⊢ ( ( 2^nd ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ↔ ( 2^nd ‘ 𝑥 ) ⊆ ∪ 𝑢 )
106	104 105	sylibr	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( 2^nd ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 )
107	103 106	jca	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → ( ( 1^st ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ) )
108		elxp6	⊢ ( 𝑥 ∈ ( 𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢 ) ↔ ( 𝑥 = ⟨ ( 1^st ‘ 𝑥 ) , ( 2^nd ‘ 𝑥 ) ⟩ ∧ ( ( 1^st ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ∧ ( 2^nd ‘ 𝑥 ) ∈ 𝒫 ∪ 𝑢 ) ) )
109	98 107 108	sylanbrc	⊢ ( ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) → 𝑥 ∈ ( 𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢 ) )
110	109	abssi	⊢ { 𝑥 ∣ ( 𝑥 ∈ ( On × On ) ∧ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ∈ 𝑢 ) } ⊆ ( 𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢 )
111	97 110	eqsstri	⊢ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ⊆ ( 𝒫 ∪ 𝑢 × 𝒫 ∪ 𝑢 )
112	94 111	ssexi	⊢ ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ∈ V
113	112	a1i	⊢ ( ⊤ → ( ^◡ ( 𝑥 ∈ ( On × On ) ↦ ( ( 1^st ‘ 𝑥 ) ∪ ( 2^nd ‘ 𝑥 ) ) ) “ 𝑢 ) ∈ V )
114	26 40 91 113	fnse	⊢ ( ⊤ → 𝑅 Se ( On × On ) )
115	89 114	jca	⊢ ( ⊤ → ( 𝑅 We ( On × On ) ∧ 𝑅 Se ( On × On ) ) )
116	115	mptru	⊢ ( 𝑅 We ( On × On ) ∧ 𝑅 Se ( On × On ) )

Metamath Proof Explorer

Theorem r0weon

Proof