Theorem inf3lema

Description: Lemma for our Axiom of Infinity => standard Axiom of Infinity. See inf3 for detailed description. (Contributed by NM, 28-Oct-1996)

	Ref	Expression
Hypotheses	inf3lem.1	⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
	inf3lem.2	⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
	inf3lem.3	⊢ 𝐴 ∈ V
	inf3lem.4	⊢ 𝐵 ∈ V
Assertion	inf3lema	⊢ ( 𝐴 ∈ ( 𝐺 ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∩ 𝑥 ) ⊆ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		inf3lem.1	⊢ 𝐺 = ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } )
2		inf3lem.2	⊢ 𝐹 = ( rec ( 𝐺 , ∅ ) ↾ ω )
3		inf3lem.3	⊢ 𝐴 ∈ V
4		inf3lem.4	⊢ 𝐵 ∈ V
5		ineq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ∩ 𝑥 ) = ( 𝐴 ∩ 𝑥 ) )
6	5	sseq1d	⊢ ( 𝑓 = 𝐴 → ( ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 ↔ ( 𝐴 ∩ 𝑥 ) ⊆ 𝐵 ) )
7		sseq2	⊢ ( 𝑣 = 𝐵 → ( ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 ↔ ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 ) )
8	7	rabbidv	⊢ ( 𝑣 = 𝐵 → { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 } = { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 } )
9		sseq2	⊢ ( 𝑦 = 𝑣 → ( ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 ↔ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑣 ) )
10	9	rabbidv	⊢ ( 𝑦 = 𝑣 → { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } = { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑣 } )
11		ineq1	⊢ ( 𝑤 = 𝑓 → ( 𝑤 ∩ 𝑥 ) = ( 𝑓 ∩ 𝑥 ) )
12	11	sseq1d	⊢ ( 𝑤 = 𝑓 → ( ( 𝑤 ∩ 𝑥 ) ⊆ 𝑣 ↔ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 ) )
13	12	cbvrabv	⊢ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑣 } = { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 }
14	10 13	eqtrdi	⊢ ( 𝑦 = 𝑣 → { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } = { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 } )
15	14	cbvmptv	⊢ ( 𝑦 ∈ V ↦ { 𝑤 ∈ 𝑥 ∣ ( 𝑤 ∩ 𝑥 ) ⊆ 𝑦 } ) = ( 𝑣 ∈ V ↦ { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 } )
16	1 15	eqtri	⊢ 𝐺 = ( 𝑣 ∈ V ↦ { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝑣 } )
17		vex	⊢ 𝑥 ∈ V
18	17	rabex	⊢ { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 } ∈ V
19	8 16 18	fvmpt	⊢ ( 𝐵 ∈ V → ( 𝐺 ‘ 𝐵 ) = { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 } )
20	4 19	ax-mp	⊢ ( 𝐺 ‘ 𝐵 ) = { 𝑓 ∈ 𝑥 ∣ ( 𝑓 ∩ 𝑥 ) ⊆ 𝐵 }
21	6 20	elrab2	⊢ ( 𝐴 ∈ ( 𝐺 ‘ 𝐵 ) ↔ ( 𝐴 ∈ 𝑥 ∧ ( 𝐴 ∩ 𝑥 ) ⊆ 𝐵 ) )