Theorem elsetrecslem

Description: Lemma for elsetrecs . Any element of setrecs ( F ) is generated by some subset of setrecs ( F ) . This is much weaker than setrec2v . To see why this lemma also requires setrec1 , consider what would happen if we replaced B with { A } . The antecedent would still hold, but the consequent would fail in general. Consider dispensing with the deduction form. (Contributed by Emmett Weisz, 11-Jul-2021) (New usage is discouraged.)

	Ref	Expression
Hypothesis	elsetrecs.1	⊢ 𝐵 = setrecs ( 𝐹 )
Assertion	elsetrecslem	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elsetrecs.1	⊢ 𝐵 = setrecs ( 𝐹 )
2		ssdifsn	⊢ ( 𝐵 ⊆ ( 𝐵 ∖ { 𝐴 } ) ↔ ( 𝐵 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝐵 ) )
3	2	simprbi	⊢ ( 𝐵 ⊆ ( 𝐵 ∖ { 𝐴 } ) → ¬ 𝐴 ∈ 𝐵 )
4	3	con2i	⊢ ( 𝐴 ∈ 𝐵 → ¬ 𝐵 ⊆ ( 𝐵 ∖ { 𝐴 } ) )
5		sseq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 ⊆ 𝐵 ↔ 𝑎 ⊆ 𝐵 ) )
6		fveq2	⊢ ( 𝑥 = 𝑎 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑎 ) )
7	6	eleq2d	⊢ ( 𝑥 = 𝑎 → ( 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ↔ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) )
8	5 7	anbi12d	⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
9	8	notbid	⊢ ( 𝑥 = 𝑎 → ( ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
10	9	spvv	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) )
11		imnan	⊢ ( ( 𝑎 ⊆ 𝐵 → ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ↔ ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) )
12		idd	⊢ ( 𝑎 ⊆ 𝐵 → ( ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) → ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) )
13		vex	⊢ 𝑎 ∈ V
14	13	a1i	⊢ ( 𝑎 ⊆ 𝐵 → 𝑎 ∈ V )
15		id	⊢ ( 𝑎 ⊆ 𝐵 → 𝑎 ⊆ 𝐵 )
16	1 14 15	setrec1	⊢ ( 𝑎 ⊆ 𝐵 → ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 )
17	12 16	jctild	⊢ ( 𝑎 ⊆ 𝐵 → ( ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
18	17	a2i	⊢ ( ( 𝑎 ⊆ 𝐵 → ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 ⊆ 𝐵 → ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
19	11 18	sylbir	⊢ ( ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 ⊆ 𝐵 → ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
20	19	adantrd	⊢ ( ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) → ( ( 𝑎 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝑎 ) → ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) ) )
21		ssdifsn	⊢ ( 𝑎 ⊆ ( 𝐵 ∖ { 𝐴 } ) ↔ ( 𝑎 ⊆ 𝐵 ∧ ¬ 𝐴 ∈ 𝑎 ) )
22		ssdifsn	⊢ ( ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐵 ∖ { 𝐴 } ) ↔ ( ( 𝐹 ‘ 𝑎 ) ⊆ 𝐵 ∧ ¬ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) )
23	20 21 22	3imtr4g	⊢ ( ¬ ( 𝑎 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑎 ) ) → ( 𝑎 ⊆ ( 𝐵 ∖ { 𝐴 } ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐵 ∖ { 𝐴 } ) ) )
24	10 23	syl	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑎 ⊆ ( 𝐵 ∖ { 𝐴 } ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐵 ∖ { 𝐴 } ) ) )
25	24	alrimiv	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑎 ( 𝑎 ⊆ ( 𝐵 ∖ { 𝐴 } ) → ( 𝐹 ‘ 𝑎 ) ⊆ ( 𝐵 ∖ { 𝐴 } ) ) )
26	1 25	setrec2v	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝐵 ⊆ ( 𝐵 ∖ { 𝐴 } ) )
27	4 26	nsyl	⊢ ( 𝐴 ∈ 𝐵 → ¬ ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
28		df-ex	⊢ ( ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) ↔ ¬ ∀ 𝑥 ¬ ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )
29	27 28	sylibr	⊢ ( 𝐴 ∈ 𝐵 → ∃ 𝑥 ( 𝑥 ⊆ 𝐵 ∧ 𝐴 ∈ ( 𝐹 ‘ 𝑥 ) ) )