dfk22 - Mathbox for BTernaryTau

	Mathbox for BTernaryTau		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > dfk22		Structured version Visualization version GIF version

Theorem dfk22 35964

Description: Alternate definition of 𝐾₂ using maps-to notation. (Contributed by BTernaryTau, 10-Oct-2026.)

**Assertion**
Ref	Expression
dfk22	⊢ 𝐾₂ = (𝑥 ∈ On ↦ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))

Proof of Theorem dfk22 Dummy variables 𝑛 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 488	. . . . 5 ⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))) → 𝑥 ∈ On)
2		simpr 490	. . . . . . . . 9 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → 𝑧 ∈ On)
3		simpllr 788	. . . . . . . . 9 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → 𝑦 ∈ On)
4		simplr 781	. . . . . . . . 9 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → 𝑛 ∈ 9_o)
5		simplll 787	. . . . . . . . 9 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → 𝑥 ∈ On)
6		eqcom 2767	. . . . . . . . . 10 ⊢ (𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) ↔ (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥)
7		otelxp 5695	. . . . . . . . . . . 12 ⊢ (⟨𝑧, 𝑦, 𝑛⟩ ∈ ((On × On) × 9_o) ↔ (𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o))
8		jf1o 35962	. . . . . . . . . . . . 13 ⊢ 𝐽:((On × On) × 9_o)–1-1-onto→On
9		f1ocnvfvb 7291	. . . . . . . . . . . . 13 ⊢ ((𝐽:((On × On) × 9_o)–1-1-onto→On ∧ ⟨𝑧, 𝑦, 𝑛⟩ ∈ ((On × On) × 9_o) ∧ 𝑥 ∈ On) → ((𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥 ↔ (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩))
10	8, 9	mp3an1 1477	. . . . . . . . . . . 12 ⊢ ((⟨𝑧, 𝑦, 𝑛⟩ ∈ ((On × On) × 9_o) ∧ 𝑥 ∈ On) → ((𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥 ↔ (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩))
11	7, 10	sylanbr 594	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o) ∧ 𝑥 ∈ On) → ((𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥 ↔ (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩))
12		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑧 ∈ V
13		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑦 ∈ V
14		vex 3454	. . . . . . . . . . . . . . 15 ⊢ 𝑛 ∈ V
15	12, 13, 14	3pm3.2i 1358	. . . . . . . . . . . . . 14 ⊢ (𝑧 ∈ V ∧ 𝑦 ∈ V ∧ 𝑛 ∈ V)
16		oteqimp 8024	. . . . . . . . . . . . . 14 ⊢ ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → ((𝑧 ∈ V ∧ 𝑦 ∈ V ∧ 𝑛 ∈ V) → ((1^st ‘(1^st ‘(^◡𝐽‘𝑥))) = 𝑧 ∧ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) = 𝑦 ∧ (2^nd ‘(^◡𝐽‘𝑥)) = 𝑛)))
17	15, 16	mpi 21	. . . . . . . . . . . . 13 ⊢ ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → ((1^st ‘(1^st ‘(^◡𝐽‘𝑥))) = 𝑧 ∧ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) = 𝑦 ∧ (2^nd ‘(^◡𝐽‘𝑥)) = 𝑛))
18	17	simp2d 1161	. . . . . . . . . . . 12 ⊢ ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) = 𝑦)
19	18	eqcomd 2766	. . . . . . . . . . 11 ⊢ ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))
20	11, 19	biimtrdi 256	. . . . . . . . . 10 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o) ∧ 𝑥 ∈ On) → ((𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥 → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
21	6, 20	biimtrid 245	. . . . . . . . 9 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o) ∧ 𝑥 ∈ On) → (𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
22	2, 3, 4, 5, 21	syl31anc 1400	. . . . . . . 8 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → (𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
23	22	rexlimdva 3163	. . . . . . 7 ⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) → (∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
24	23	rexlimdva 3163	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
25	24	impr 460	. . . . 5 ⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))) → 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))
26	1, 25	jca 521	. . . 4 ⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))) → (𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
27		f1ocnvdm 7297	. . . . . . . . . 10 ⊢ ((𝐽:((On × On) × 9_o)–1-1-onto→On ∧ 𝑥 ∈ On) → (^◡𝐽‘𝑥) ∈ ((On × On) × 9_o))
28	8, 27	mpan 703	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (^◡𝐽‘𝑥) ∈ ((On × On) × 9_o))
29		xp1st 8037	. . . . . . . . 9 ⊢ ((^◡𝐽‘𝑥) ∈ ((On × On) × 9_o) → (1^st ‘(^◡𝐽‘𝑥)) ∈ (On × On))
30		xp2nd 8038	. . . . . . . . 9 ⊢ ((1^st ‘(^◡𝐽‘𝑥)) ∈ (On × On) → (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
31	28, 29, 30	3syl 19	. . . . . . . 8 ⊢ (𝑥 ∈ On → (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
32	31	adantr 486	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
33		eleq1 2848	. . . . . . . 8 ⊢ (𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) → (𝑦 ∈ On ↔ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On))
34	33	adantl 487	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (𝑦 ∈ On ↔ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On))
35	32, 34	mpbird 260	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → 𝑦 ∈ On)
36		oteq3 4861	. . . . . . . . 9 ⊢ (𝑛 = (2^nd ‘(^◡𝐽‘𝑥)) → ⟨𝑧, 𝑦, 𝑛⟩ = ⟨𝑧, 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩)
37	36	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑛 = (2^nd ‘(^◡𝐽‘𝑥)) → ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ ↔ (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩))
38		oteq1 4859	. . . . . . . . 9 ⊢ (𝑧 = (1^st ‘(1^st ‘(^◡𝐽‘𝑥))) → ⟨𝑧, 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩ = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩)
39	38	eqeq2d 2771	. . . . . . . 8 ⊢ (𝑧 = (1^st ‘(1^st ‘(^◡𝐽‘𝑥))) → ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩ ↔ (^◡𝐽‘𝑥) = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩))
40		xp2nd 8038	. . . . . . . . . 10 ⊢ ((^◡𝐽‘𝑥) ∈ ((On × On) × 9_o) → (2^nd ‘(^◡𝐽‘𝑥)) ∈ 9_o)
41	28, 40	syl 18	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (2^nd ‘(^◡𝐽‘𝑥)) ∈ 9_o)
42	41	adantr 486	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (2^nd ‘(^◡𝐽‘𝑥)) ∈ 9_o)
43		xp1st 8037	. . . . . . . . . 10 ⊢ ((1^st ‘(^◡𝐽‘𝑥)) ∈ (On × On) → (1^st ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
44	28, 29, 43	3syl 19	. . . . . . . . 9 ⊢ (𝑥 ∈ On → (1^st ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
45	44	adantr 486	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (1^st ‘(1^st ‘(^◡𝐽‘𝑥))) ∈ On)
46		ot1st2nd 35772	. . . . . . . . . . 11 ⊢ ((^◡𝐽‘𝑥) ∈ ((On × On) × 9_o) → (^◡𝐽‘𝑥) = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(^◡𝐽‘𝑥))⟩)
47	28, 46	syl 18	. . . . . . . . . 10 ⊢ (𝑥 ∈ On → (^◡𝐽‘𝑥) = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(^◡𝐽‘𝑥))⟩)
48	47	adantr 486	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (^◡𝐽‘𝑥) = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(^◡𝐽‘𝑥))⟩)
49		oteq2 4860	. . . . . . . . . 10 ⊢ (𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))) → ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩ = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(^◡𝐽‘𝑥))⟩)
50	49	adantl 487	. . . . . . . . 9 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩ = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))), (2^nd ‘(^◡𝐽‘𝑥))⟩)
51	48, 50	eqtr4d 2798	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (^◡𝐽‘𝑥) = ⟨(1^st ‘(1^st ‘(^◡𝐽‘𝑥))), 𝑦, (2^nd ‘(^◡𝐽‘𝑥))⟩)
52	37, 39, 42, 45, 51	2rspcedvdw 3589	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → ∃𝑛 ∈ 9_o ∃𝑧 ∈ On (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩)
53	11	biimprd 251	. . . . . . . . . . . 12 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o) ∧ 𝑥 ∈ On) → ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) = 𝑥))
54	53, 6	imbitrrdi 255	. . . . . . . . . . 11 ⊢ (((𝑧 ∈ On ∧ 𝑦 ∈ On ∧ 𝑛 ∈ 9_o) ∧ 𝑥 ∈ On) → ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
55	2, 3, 4, 5, 54	syl31anc 1400	. . . . . . . . . 10 ⊢ ((((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) ∧ 𝑧 ∈ On) → ((^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
56	55	reximdva 3175	. . . . . . . . 9 ⊢ (((𝑥 ∈ On ∧ 𝑦 ∈ On) ∧ 𝑛 ∈ 9_o) → (∃𝑧 ∈ On (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
57	56	reximdva 3175	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ On) → (∃𝑛 ∈ 9_o ∃𝑧 ∈ On (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
58	35, 57	syldan 603	. . . . . . 7 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (∃𝑛 ∈ 9_o ∃𝑧 ∈ On (^◡𝐽‘𝑥) = ⟨𝑧, 𝑦, 𝑛⟩ → ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
59	52, 58	mpd 16	. . . . . 6 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))
60	35, 59	jca 521	. . . . 5 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))
61		f1of 6829	. . . . . . . . . . 11 ⊢ (𝐽:((On × On) × 9_o)–1-1-onto→On → 𝐽:((On × On) × 9_o)⟶On)
62	8, 61	ax-mp 5	. . . . . . . . . 10 ⊢ 𝐽:((On × On) × 9_o)⟶On
63		0elon 6421	. . . . . . . . . 10 ⊢ ∅ ∈ On
64	62, 63	f0cli 7103	. . . . . . . . 9 ⊢ (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) ∈ On
65		eleq1 2848	. . . . . . . . 9 ⊢ (𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → (𝑥 ∈ On ↔ (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) ∈ On))
66	64, 65	mpbiri 261	. . . . . . . 8 ⊢ (𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑥 ∈ On)
67	66	rexlimivw 3159	. . . . . . 7 ⊢ (∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑥 ∈ On)
68	67	rexlimivw 3159	. . . . . 6 ⊢ (∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩) → 𝑥 ∈ On)
69	68	adantl 487	. . . . 5 ⊢ ((𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)) → 𝑥 ∈ On)
70	60, 69	jccil 532	. . . 4 ⊢ ((𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) → (𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))))
71	26, 70	impbii 212	. . 3 ⊢ ((𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))) ↔ (𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))))
72	71	opabbii 5171	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))}
73		df-k2 35945	. . 3 ⊢ 𝐾₂ = {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))}
74	69	pm4.71ri 570	. . . 4 ⊢ ((𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)) ↔ (𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))))
75	74	opabbii 5171	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩))} = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))}
76	73, 75	eqtri 2783	. 2 ⊢ 𝐾₂ = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ On ∧ (𝑦 ∈ On ∧ ∃𝑛 ∈ 9_o ∃𝑧 ∈ On 𝑥 = (𝐽‘⟨𝑧, 𝑦, 𝑛⟩)))}
77		df-mpt 5186	. 2 ⊢ (𝑥 ∈ On ↦ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥)))) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ On ∧ 𝑦 = (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))}
78	72, 76, 77	3eqtr4i 2793	1 ⊢ 𝐾₂ = (𝑥 ∈ On ↦ (2^nd ‘(1^st ‘(^◡𝐽‘𝑥))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1569 ∈ wcel 2144 ∃wrex 3086 Vcvv 3450 ⟨cotp 4857 {copab 5166 ↦ cmpt 5185 × cxp 5649 ^◡ccnv 5650 Oncon0 6365 ⟶wf 6539 –1-1-onto→wf1o 6542 ‘cfv 6543 1^st c1st 8003 2^nd c2nd 8004 9_oc9o 35833 𝐽cj 35934 𝐾₂ck2 35936

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5327 ax-pr 5391 ax-un 7755

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3848 df-ss 3897 df-pss 4013 df-dif 4046 df-in 4090 df-un 4150 df-nul 4278 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-op 4835 df-ot 4858 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5546 df-eprel 5551 df-po 5559 df-so 5560 df-fr 5604 df-se 5605 df-we 5606 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-pred 6307 df-ord 6368 df-on 6369 df-lim 6370 df-suc 6371 df-iota 6497 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-isom 6552 df-riota 7381 df-ov 7427 df-oprab 7428 df-mpo 7429 df-mpt3 7688 df-om 7882 df-1st 8005 df-2nd 8006 df-frecs 8307 df-wrecs 8338 df-recs 8387 df-rdg 8426 df-1o 8484 df-2o 8485 df-3o 8486 df-4o 8487 df-oadd 8488 df-omul 8489 df-oi 9511 df-5o 35834 df-6o 35835 df-7o 35836 df-8o 35837 df-9o 35838 df-lexo 35940 df-r0 35941 df-j0 35942 df-j 35943 df-k2 35945

This theorem is used by: k2on 35967 jk1k2k3 35969

W3C validator