Theorem nelsubclem

Description: Lemma for nelsubc . (Contributed by Zhi Wang, 5-Nov-2025)

	Ref	Expression
Hypotheses	nelsubc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	nelsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
	nelsubc.0	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
	nelsubc.j	⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
	nelsubc.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
Assertion	nelsubclem	⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		nelsubc.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		nelsubc.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐵 )
3		nelsubc.0	⊢ ( 𝜑 → 𝑆 ≠ ∅ )
4		nelsubc.j	⊢ ( 𝜑 → 𝐽 = ( ( 𝑆 × 𝑆 ) × { ∅ } ) )
5		nelsubc.h	⊢ 𝐻 = ( Homf ‘ 𝐶 )
6		0ex	⊢ ∅ ∈ V
7		fnconstg	⊢ ( ∅ ∈ V → ( ( 𝑆 × 𝑆 ) × { ∅ } ) Fn ( 𝑆 × 𝑆 ) )
8	6 7	ax-mp	⊢ ( ( 𝑆 × 𝑆 ) × { ∅ } ) Fn ( 𝑆 × 𝑆 )
9	4	fneq1d	⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ↔ ( ( 𝑆 × 𝑆 ) × { ∅ } ) Fn ( 𝑆 × 𝑆 ) ) )
10	8 9	mpbiri	⊢ ( 𝜑 → 𝐽 Fn ( 𝑆 × 𝑆 ) )
11	4	oveqd	⊢ ( 𝜑 → ( 𝑝 𝐽 𝑞 ) = ( 𝑝 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑞 ) )
12	6	ovconst2	⊢ ( ( 𝑝 ∈ 𝑆 ∧ 𝑞 ∈ 𝑆 ) → ( 𝑝 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑞 ) = ∅ )
13	11 12	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑆 ∧ 𝑞 ∈ 𝑆 ) ) → ( 𝑝 𝐽 𝑞 ) = ∅ )
14		0ss	⊢ ∅ ⊆ ( 𝑝 𝐻 𝑞 )
15	13 14	eqsstrdi	⊢ ( ( 𝜑 ∧ ( 𝑝 ∈ 𝑆 ∧ 𝑞 ∈ 𝑆 ) ) → ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) )
16	15	ralrimivva	⊢ ( 𝜑 → ∀ 𝑝 ∈ 𝑆 ∀ 𝑞 ∈ 𝑆 ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) )
17	5 1	homffn	⊢ 𝐻 Fn ( 𝐵 × 𝐵 )
18	17	a1i	⊢ ( 𝜑 → 𝐻 Fn ( 𝐵 × 𝐵 ) )
19	1	fvexi	⊢ 𝐵 ∈ V
20	19	a1i	⊢ ( 𝜑 → 𝐵 ∈ V )
21	10 18 20	isssc	⊢ ( 𝜑 → ( 𝐽 ⊆cat 𝐻 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∀ 𝑝 ∈ 𝑆 ∀ 𝑞 ∈ 𝑆 ( 𝑝 𝐽 𝑞 ) ⊆ ( 𝑝 𝐻 𝑞 ) ) ) )
22	2 16 21	mpbir2and	⊢ ( 𝜑 → 𝐽 ⊆cat 𝐻 )
23	4	oveqd	⊢ ( 𝜑 → ( 𝑥 𝐽 𝑥 ) = ( 𝑥 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑥 ) )
24	6	ovconst2	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑥 ) = ∅ )
25	24	anidms	⊢ ( 𝑥 ∈ 𝑆 → ( 𝑥 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑥 ) = ∅ )
26	23 25	sylan9eq	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 𝐽 𝑥 ) = ∅ )
27		nel02	⊢ ( ( 𝑥 𝐽 𝑥 ) = ∅ → ¬ 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
28	26 27	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ¬ 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
29	28	reximdva0	⊢ ( ( 𝜑 ∧ 𝑆 ≠ ∅ ) → ∃ 𝑥 ∈ 𝑆 ¬ 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
30	3 29	mpdan	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑆 ¬ 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
31		rexnal	⊢ ( ∃ 𝑥 ∈ 𝑆 ¬ 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ 𝑆 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
32	30 31	sylib	⊢ ( 𝜑 → ¬ ∀ 𝑥 ∈ 𝑆 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) )
33	4	oveqd	⊢ ( 𝜑 → ( 𝑥 𝐽 𝑦 ) = ( 𝑥 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑦 ) )
34	6	ovconst2	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( ( 𝑆 × 𝑆 ) × { ∅ } ) 𝑦 ) = ∅ )
35	33 34	sylan9eq	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 𝐽 𝑦 ) = ∅ )
36		rzal	⊢ ( ( 𝑥 𝐽 𝑦 ) = ∅ → ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 )
37	35 36	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 )
38	37	ralrimivw	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 )
39	38	ralrimivva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 )
40	32 39	jca	⊢ ( 𝜑 → ( ¬ ∀ 𝑥 ∈ 𝑆 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 ) )
41	10 22 40	jca32	⊢ ( 𝜑 → ( 𝐽 Fn ( 𝑆 × 𝑆 ) ∧ ( 𝐽 ⊆cat 𝐻 ∧ ( ¬ ∀ 𝑥 ∈ 𝑆 𝐼 ∈ ( 𝑥 𝐽 𝑥 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ∀ 𝑧 ∈ 𝑆 ∀ 𝑓 ∈ ( 𝑥 𝐽 𝑦 ) 𝜓 ) ) ) )