Theorem onvf1odlem2

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

	Ref	Expression
Hypotheses	onvf1odlem2.1	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
	onvf1odlem2.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 }
	onvf1odlem2.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) )
Assertion	onvf1odlem2	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → 𝑁 ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		onvf1odlem2.1	⊢ ( 𝜑 → ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) )
2		onvf1odlem2.2	⊢ 𝑀 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 }
3		onvf1odlem2.3	⊢ 𝑁 = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) )
4		onvf1odlem1	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 )
5		nfcv	⊢ Ⅎ 𝑥 𝑅1
6		nfrab1	⊢ Ⅎ 𝑥 { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 }
7	6	nfint	⊢ Ⅎ 𝑥 ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 }
8	5 7	nffv	⊢ Ⅎ 𝑥 ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } )
9		nfv	⊢ Ⅎ 𝑥 ¬ 𝑣 ∈ 𝐴
10	8 9	nfrexw	⊢ Ⅎ 𝑥 ∃ 𝑣 ∈ ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) ¬ 𝑣 ∈ 𝐴
11		eleq1w	⊢ ( 𝑦 = 𝑣 → ( 𝑦 ∈ 𝐴 ↔ 𝑣 ∈ 𝐴 ) )
12	11	notbid	⊢ ( 𝑦 = 𝑣 → ( ¬ 𝑦 ∈ 𝐴 ↔ ¬ 𝑣 ∈ 𝐴 ) )
13	12	cbvrexvw	⊢ ( ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑣 ∈ 𝐴 )
14		fveq2	⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } → ( 𝑅1 ‘ 𝑥 ) = ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) )
15	14	rexeqdv	⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } → ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑣 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) ¬ 𝑣 ∈ 𝐴 ) )
16	13 15	bitrid	⊢ ( 𝑥 = ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } → ( ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) ¬ 𝑣 ∈ 𝐴 ) )
17	10 16	onminsb	⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 → ∃ 𝑣 ∈ ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) ¬ 𝑣 ∈ 𝐴 )
18	2	fveq2i	⊢ ( 𝑅1 ‘ 𝑀 ) = ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } )
19	18	rexeqi	⊢ ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ¬ 𝑣 ∈ 𝐴 ↔ ∃ 𝑣 ∈ ( 𝑅1 ‘ ∩ { 𝑥 ∈ On ∣ ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 } ) ¬ 𝑣 ∈ 𝐴 )
20	17 19	sylibr	⊢ ( ∃ 𝑥 ∈ On ∃ 𝑦 ∈ ( 𝑅1 ‘ 𝑥 ) ¬ 𝑦 ∈ 𝐴 → ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ¬ 𝑣 ∈ 𝐴 )
21	4 20	syl	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ¬ 𝑣 ∈ 𝐴 )
22		df-rex	⊢ ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ¬ 𝑣 ∈ 𝐴 ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ∧ ¬ 𝑣 ∈ 𝐴 ) )
23		nss	⊢ ( ¬ ( 𝑅1 ‘ 𝑀 ) ⊆ 𝐴 ↔ ∃ 𝑣 ( 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ∧ ¬ 𝑣 ∈ 𝐴 ) )
24		ssdif0	⊢ ( ( 𝑅1 ‘ 𝑀 ) ⊆ 𝐴 ↔ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) = ∅ )
25	24	necon3bbii	⊢ ( ¬ ( 𝑅1 ‘ 𝑀 ) ⊆ 𝐴 ↔ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ )
26	22 23 25	3bitr2i	⊢ ( ∃ 𝑣 ∈ ( 𝑅1 ‘ 𝑀 ) ¬ 𝑣 ∈ 𝐴 ↔ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ )
27	21 26	sylib	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ )
28		fvex	⊢ ( 𝑅1 ‘ 𝑀 ) ∈ V
29	28	difexi	⊢ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ∈ V
30		neeq1	⊢ ( 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) → ( 𝑧 ≠ ∅ ↔ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ ) )
31		fveq2	⊢ ( 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )
32		id	⊢ ( 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) → 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) )
33	31 32	eleq12d	⊢ ( 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) → ( ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )
34	30 33	imbi12d	⊢ ( 𝑧 = ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) → ( ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ → ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ) )
35	29 34	spcv	⊢ ( ∀ 𝑧 ( 𝑧 ≠ ∅ → ( 𝐺 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ≠ ∅ → ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )
36	1 27 35	syl2im	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )
37	3	eleq1i	⊢ ( 𝑁 ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ↔ ( 𝐺 ‘ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) )
38	36 37	imbitrrdi	⊢ ( 𝜑 → ( 𝐴 ∈ 𝑉 → 𝑁 ∈ ( ( 𝑅1 ‘ 𝑀 ) ∖ 𝐴 ) ) )