Theorem onvf1odlem1

Description: Lemma for onvf1od . (Contributed by BTernaryTau, 2-Dec-2025)

	Ref	Expression
Assertion	onvf1odlem1	|- ( A e. V -> E. x e. On E. y e. ( R1 ` x ) -. y e. A )

Proof

Step	Hyp	Ref	Expression
1		nvel	|- -. _V e. V
2		eleq1	|- ( _V = A -> ( _V e. V <-> A e. V ) )
3	2	eqcoms	|- ( A = _V -> ( _V e. V <-> A e. V ) )
4	1 3	mtbii	|- ( A = _V -> -. A e. V )
5	4	con2i	|- ( A e. V -> -. A = _V )
6		eqv	|- ( A = _V <-> A. y y e. A )
7		alex	|- ( A. y y e. A <-> -. E. y -. y e. A )
8	6 7	bitri	|- ( A = _V <-> -. E. y -. y e. A )
9	8	con2bii	|- ( E. y -. y e. A <-> -. A = _V )
10	5 9	sylibr	|- ( A e. V -> E. y -. y e. A )
11		ax-1	|- ( -. y e. A -> ( x e. On -> -. y e. A ) )
12	11	ralrimiv	|- ( -. y e. A -> A. x e. On -. y e. A )
13	12	eximi	|- ( E. y -. y e. A -> E. y A. x e. On -. y e. A )
14		rexv	|- ( E. y e. _V A. x e. On -. y e. A <-> E. y A. x e. On -. y e. A )
15	13 14	sylibr	|- ( E. y -. y e. A -> E. y e. _V A. x e. On -. y e. A )
16		tz9.13g	|- ( y e. _V -> E. x e. On y e. ( R1 ` x ) )
17	16	rgen	|- A. y e. _V E. x e. On y e. ( R1 ` x )
18		r19.29r	|- ( ( E. y e. _V A. x e. On -. y e. A /\ A. y e. _V E. x e. On y e. ( R1 ` x ) ) -> E. y e. _V ( A. x e. On -. y e. A /\ E. x e. On y e. ( R1 ` x ) ) )
19		r19.29	|- ( ( A. x e. On -. y e. A /\ E. x e. On y e. ( R1 ` x ) ) -> E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) )
20	19	reximi	|- ( E. y e. _V ( A. x e. On -. y e. A /\ E. x e. On y e. ( R1 ` x ) ) -> E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) )
21	18 20	syl	|- ( ( E. y e. _V A. x e. On -. y e. A /\ A. y e. _V E. x e. On y e. ( R1 ` x ) ) -> E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) )
22	17 21	mpan2	|- ( E. y e. _V A. x e. On -. y e. A -> E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) )
23	10 15 22	3syl	|- ( A e. V -> E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) )
24		rexcom	|- ( E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. x e. On E. y e. _V ( -. y e. A /\ y e. ( R1 ` x ) ) )
25		exancom	|- ( E. y ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. y ( y e. ( R1 ` x ) /\ -. y e. A ) )
26		rexv	|- ( E. y e. _V ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. y ( -. y e. A /\ y e. ( R1 ` x ) ) )
27		df-rex	|- ( E. y e. ( R1 ` x ) -. y e. A <-> E. y ( y e. ( R1 ` x ) /\ -. y e. A ) )
28	25 26 27	3bitr4i	|- ( E. y e. _V ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. y e. ( R1 ` x ) -. y e. A )
29	28	rexbii	|- ( E. x e. On E. y e. _V ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. x e. On E. y e. ( R1 ` x ) -. y e. A )
30	24 29	bitri	|- ( E. y e. _V E. x e. On ( -. y e. A /\ y e. ( R1 ` x ) ) <-> E. x e. On E. y e. ( R1 ` x ) -. y e. A )
31	23 30	sylib	|- ( A e. V -> E. x e. On E. y e. ( R1 ` x ) -. y e. A )