Theorem modelaxreplem1

Description: Lemma for modelaxrep . We show that M is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypotheses	modelaxreplem.1	⊢ ( 𝜓 → 𝑥 ⊆ 𝑀 )
	modelaxreplem.2	⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) )
	modelaxreplem.3	⊢ ( 𝜓 → ∅ ∈ 𝑀 )
	modelaxreplem.4	⊢ ( 𝜓 → 𝑥 ∈ 𝑀 )
	modelaxreplem1.5	⊢ 𝐴 ⊆ 𝑥
Assertion	modelaxreplem1	⊢ ( 𝜓 → 𝐴 ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		modelaxreplem.1	⊢ ( 𝜓 → 𝑥 ⊆ 𝑀 )
2		modelaxreplem.2	⊢ ( 𝜓 → ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) )
3		modelaxreplem.3	⊢ ( 𝜓 → ∅ ∈ 𝑀 )
4		modelaxreplem.4	⊢ ( 𝜓 → 𝑥 ∈ 𝑀 )
5		modelaxreplem1.5	⊢ 𝐴 ⊆ 𝑥
6		eleq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ∈ 𝑀 ↔ ∅ ∈ 𝑀 ) )
7	3 6	syl5ibrcom	⊢ ( 𝜓 → ( 𝐴 = ∅ → 𝐴 ∈ 𝑀 ) )
8		vex	⊢ 𝑥 ∈ V
9	8 5	ssexi	⊢ 𝐴 ∈ V
10	9	0sdom	⊢ ( ∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅ )
11		ssdomg	⊢ ( 𝑥 ∈ V → ( 𝐴 ⊆ 𝑥 → 𝐴 ≼ 𝑥 ) )
12	8 5 11	mp2	⊢ 𝐴 ≼ 𝑥
13		fodomr	⊢ ( ( ∅ ≺ 𝐴 ∧ 𝐴 ≼ 𝑥 ) → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 )
14	12 13	mpan2	⊢ ( ∅ ≺ 𝐴 → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 )
15	10 14	sylbir	⊢ ( 𝐴 ≠ ∅ → ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 )
16		df-fo	⊢ ( 𝑔 : 𝑥 –onto→ 𝐴 ↔ ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) )
17		df-fn	⊢ ( 𝑔 Fn 𝑥 ↔ ( Fun 𝑔 ∧ dom 𝑔 = 𝑥 ) )
18		eleq1	⊢ ( dom 𝑔 = 𝑥 → ( dom 𝑔 ∈ 𝑀 ↔ 𝑥 ∈ 𝑀 ) )
19	4 18	syl5ibrcom	⊢ ( 𝜓 → ( dom 𝑔 = 𝑥 → dom 𝑔 ∈ 𝑀 ) )
20	19	anim2d	⊢ ( 𝜓 → ( ( Fun 𝑔 ∧ dom 𝑔 = 𝑥 ) → ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ) )
21	17 20	biimtrid	⊢ ( 𝜓 → ( 𝑔 Fn 𝑥 → ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ) )
22	5 1	sstrid	⊢ ( 𝜓 → 𝐴 ⊆ 𝑀 )
23		sseq1	⊢ ( ran 𝑔 = 𝐴 → ( ran 𝑔 ⊆ 𝑀 ↔ 𝐴 ⊆ 𝑀 ) )
24	22 23	syl5ibrcom	⊢ ( 𝜓 → ( ran 𝑔 = 𝐴 → ran 𝑔 ⊆ 𝑀 ) )
25		df-3an	⊢ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ∧ ran 𝑔 ⊆ 𝑀 ) )
26		funeq	⊢ ( 𝑓 = 𝑔 → ( Fun 𝑓 ↔ Fun 𝑔 ) )
27		dmeq	⊢ ( 𝑓 = 𝑔 → dom 𝑓 = dom 𝑔 )
28	27	eleq1d	⊢ ( 𝑓 = 𝑔 → ( dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀 ) )
29		rneq	⊢ ( 𝑓 = 𝑔 → ran 𝑓 = ran 𝑔 )
30	29	sseq1d	⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀 ) )
31	26 28 30	3anbi123d	⊢ ( 𝑓 = 𝑔 → ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) ↔ ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) ) )
32	29	eleq1d	⊢ ( 𝑓 = 𝑔 → ( ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀 ) )
33	31 32	imbi12d	⊢ ( 𝑓 = 𝑔 → ( ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) ↔ ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) ) )
34	33	spvv	⊢ ( ∀ 𝑓 ( ( Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀 ) → ran 𝑓 ∈ 𝑀 ) → ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) )
35	2 34	syl	⊢ ( 𝜓 → ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) )
36	25 35	biimtrrid	⊢ ( 𝜓 → ( ( ( Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ) ∧ ran 𝑔 ⊆ 𝑀 ) → ran 𝑔 ∈ 𝑀 ) )
37	21 24 36	syl2and	⊢ ( 𝜓 → ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → ran 𝑔 ∈ 𝑀 ) )
38		eleq1	⊢ ( ran 𝑔 = 𝐴 → ( ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀 ) )
39	38	adantl	⊢ ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → ( ran 𝑔 ∈ 𝑀 ↔ 𝐴 ∈ 𝑀 ) )
40	37 39	mpbidi	⊢ ( 𝜓 → ( ( 𝑔 Fn 𝑥 ∧ ran 𝑔 = 𝐴 ) → 𝐴 ∈ 𝑀 ) )
41	16 40	biimtrid	⊢ ( 𝜓 → ( 𝑔 : 𝑥 –onto→ 𝐴 → 𝐴 ∈ 𝑀 ) )
42	41	exlimdv	⊢ ( 𝜓 → ( ∃ 𝑔 𝑔 : 𝑥 –onto→ 𝐴 → 𝐴 ∈ 𝑀 ) )
43	15 42	syl5	⊢ ( 𝜓 → ( 𝐴 ≠ ∅ → 𝐴 ∈ 𝑀 ) )
44	7 43	pm2.61dne	⊢ ( 𝜓 → 𝐴 ∈ 𝑀 )