Theorem fsplitOLD

Description: Obsolete proof of fsplit as of 31-Dec-2023. (Contributed by NM, 17-Sep-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	fsplitOLD	⊢ ◡ ( 1st ↾ I ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ )

Proof

Step	Hyp	Ref	Expression
1		vex	⊢ 𝑥 ∈ V
2		vex	⊢ 𝑦 ∈ V
3	1 2	brcnv	⊢ ( 𝑥 ◡ ( 1st ↾ I ) 𝑦 ↔ 𝑦 ( 1st ↾ I ) 𝑥 )
4	1	brresi	⊢ ( 𝑦 ( 1st ↾ I ) 𝑥 ↔ ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) )
5		19.42v	⊢ ( ∃ 𝑧 ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
6		vex	⊢ 𝑧 ∈ V
7	6 6	op1std	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ → ( 1st ‘ 𝑦 ) = 𝑧 )
8	7	eqeq1d	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ → ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑧 = 𝑥 ) )
9	8	pm5.32ri	⊢ ( ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
10	9	exbii	⊢ ( ∃ 𝑧 ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
11		fo1st	⊢ 1st : V –onto→ V
12		fofn	⊢ ( 1st : V –onto→ V → 1st Fn V )
13	11 12	ax-mp	⊢ 1st Fn V
14		fnbrfvb	⊢ ( ( 1st Fn V ∧ 𝑦 ∈ V ) → ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑦 1st 𝑥 ) )
15	13 2 14	mp2an	⊢ ( ( 1st ‘ 𝑦 ) = 𝑥 ↔ 𝑦 1st 𝑥 )
16		dfid2	⊢ I = { ⟨ 𝑧 , 𝑧 ⟩ ∣ 𝑧 = 𝑧 }
17	16	eleq2i	⊢ ( 𝑦 ∈ I ↔ 𝑦 ∈ { ⟨ 𝑧 , 𝑧 ⟩ ∣ 𝑧 = 𝑧 } )
18		nfe1	⊢ Ⅎ 𝑧 ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 )
19	18	19.9	⊢ ( ∃ 𝑧 ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 ) ↔ ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 ) )
20		elopab	⊢ ( 𝑦 ∈ { ⟨ 𝑧 , 𝑧 ⟩ ∣ 𝑧 = 𝑧 } ↔ ∃ 𝑧 ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 ) )
21		equid	⊢ 𝑧 = 𝑧
22	21	biantru	⊢ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 ) )
23	22	exbii	⊢ ( ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ ∃ 𝑧 ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ∧ 𝑧 = 𝑧 ) )
24	19 20 23	3bitr4i	⊢ ( 𝑦 ∈ { ⟨ 𝑧 , 𝑧 ⟩ ∣ 𝑧 = 𝑧 } ↔ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ )
25	17 24	bitr2i	⊢ ( ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ 𝑦 ∈ I )
26	15 25	anbi12ci	⊢ ( ( ( 1st ‘ 𝑦 ) = 𝑥 ∧ ∃ 𝑧 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) )
27	5 10 26	3bitr3ri	⊢ ( ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) ↔ ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) )
28		id	⊢ ( 𝑧 = 𝑥 → 𝑧 = 𝑥 )
29	28 28	opeq12d	⊢ ( 𝑧 = 𝑥 → ⟨ 𝑧 , 𝑧 ⟩ = ⟨ 𝑥 , 𝑥 ⟩ )
30	29	eqeq2d	⊢ ( 𝑧 = 𝑥 → ( 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ ) )
31	30	equsexvw	⊢ ( ∃ 𝑧 ( 𝑧 = 𝑥 ∧ 𝑦 = ⟨ 𝑧 , 𝑧 ⟩ ) ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
32	27 31	bitri	⊢ ( ( 𝑦 ∈ I ∧ 𝑦 1st 𝑥 ) ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
33	4 32	bitri	⊢ ( 𝑦 ( 1st ↾ I ) 𝑥 ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
34	3 33	bitri	⊢ ( 𝑥 ◡ ( 1st ↾ I ) 𝑦 ↔ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ )
35	34	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ }
36		relcnv	⊢ Rel ◡ ( 1st ↾ I )
37		dfrel4v	⊢ ( Rel ◡ ( 1st ↾ I ) ↔ ◡ ( 1st ↾ I ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 } )
38	36 37	mpbi	⊢ ◡ ( 1st ↾ I ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 ◡ ( 1st ↾ I ) 𝑦 }
39		mptv	⊢ ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑦 = ⟨ 𝑥 , 𝑥 ⟩ }
40	35 38 39	3eqtr4i	⊢ ◡ ( 1st ↾ I ) = ( 𝑥 ∈ V ↦ ⟨ 𝑥 , 𝑥 ⟩ )