Theorem regsfromunir1

Description: Derivation of ax-regs from unir1 . (Contributed by Matthew House, 4-Mar-2026)

	Ref	Expression
Hypothesis	regsfromunir1.1	⊢ ∪ ( 𝑅1 “ On ) = V
Assertion	regsfromunir1	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		regsfromunir1.1	⊢ ∪ ( 𝑅1 “ On ) = V
2		rankf	⊢ rank : ∪ ( 𝑅1 “ On ) ⟶ On
3		fimass	⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → ( rank “ { 𝑥 ∣ 𝜑 } ) ⊆ On )
4	2 3	ax-mp	⊢ ( rank “ { 𝑥 ∣ 𝜑 } ) ⊆ On
5		ffn	⊢ ( rank : ∪ ( 𝑅1 “ On ) ⟶ On → rank Fn ∪ ( 𝑅1 “ On ) )
6	2 5	ax-mp	⊢ rank Fn ∪ ( 𝑅1 “ On )
7		ssv	⊢ { 𝑥 ∣ 𝜑 } ⊆ V
8	7 1	sseqtrri	⊢ { 𝑥 ∣ 𝜑 } ⊆ ∪ ( 𝑅1 “ On )
9		fnimaeq0	⊢ ( ( rank Fn ∪ ( 𝑅1 “ On ) ∧ { 𝑥 ∣ 𝜑 } ⊆ ∪ ( 𝑅1 “ On ) ) → ( ( rank “ { 𝑥 ∣ 𝜑 } ) = ∅ ↔ { 𝑥 ∣ 𝜑 } = ∅ ) )
10	6 8 9	mp2an	⊢ ( ( rank “ { 𝑥 ∣ 𝜑 } ) = ∅ ↔ { 𝑥 ∣ 𝜑 } = ∅ )
11	10	necon3bii	⊢ ( ( rank “ { 𝑥 ∣ 𝜑 } ) ≠ ∅ ↔ { 𝑥 ∣ 𝜑 } ≠ ∅ )
12	11	biimpri	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ → ( rank “ { 𝑥 ∣ 𝜑 } ) ≠ ∅ )
13		onint	⊢ ( ( ( rank “ { 𝑥 ∣ 𝜑 } ) ⊆ On ∧ ( rank “ { 𝑥 ∣ 𝜑 } ) ≠ ∅ ) → ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) )
14	4 12 13	sylancr	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ → ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) )
15		abn0	⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
16		fvelimab	⊢ ( ( rank Fn ∪ ( 𝑅1 “ On ) ∧ { 𝑥 ∣ 𝜑 } ⊆ ∪ ( 𝑅1 “ On ) ) → ( ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ) )
17	6 8 16	mp2an	⊢ ( ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) )
18	14 15 17	3imtr3i	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) )
19		vex	⊢ 𝑦 ∈ V
20	19 1	eleqtrri	⊢ 𝑦 ∈ ∪ ( 𝑅1 “ On )
21		rankelb	⊢ ( 𝑦 ∈ ∪ ( 𝑅1 “ On ) → ( 𝑧 ∈ 𝑦 → ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑦 ) ) )
22	20 21	ax-mp	⊢ ( 𝑧 ∈ 𝑦 → ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑦 ) )
23		eleq2	⊢ ( ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑧 ) ∈ ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ) )
24	23	biimpd	⊢ ( ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ( ( rank ‘ 𝑧 ) ∈ ( rank ‘ 𝑦 ) → ( rank ‘ 𝑧 ) ∈ ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) ) )
25		fnfvima	⊢ ( ( rank Fn ∪ ( 𝑅1 “ On ) ∧ { 𝑥 ∣ 𝜑 } ⊆ ∪ ( 𝑅1 “ On ) ∧ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) → ( rank ‘ 𝑧 ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) )
26	6 8 25	mp3an12	⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑧 ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) )
27		onnmin	⊢ ( ( ( rank “ { 𝑥 ∣ 𝜑 } ) ⊆ On ∧ ( rank ‘ 𝑧 ) ∈ ( rank “ { 𝑥 ∣ 𝜑 } ) ) → ¬ ( rank ‘ 𝑧 ) ∈ ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) )
28	4 26 27	sylancr	⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } → ¬ ( rank ‘ 𝑧 ) ∈ ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) )
29	28	con2i	⊢ ( ( rank ‘ 𝑧 ) ∈ ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } )
30	22 24 29	syl56	⊢ ( ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
31	30	alrimiv	⊢ ( ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
32	31	reximi	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑦 ) = ∩ ( rank “ { 𝑥 ∣ 𝜑 } ) → ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) )
33		df-rex	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∃ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) )
34		df-clab	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑦 / 𝑥 ] 𝜑 )
35		sb6	⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
36	34 35	bitri	⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) )
37		df-clab	⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 )
38		sb6	⊢ ( [ 𝑧 / 𝑥 ] 𝜑 ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
39	37 38	bitri	⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
40	39	notbii	⊢ ( ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) )
41	40	imbi2i	⊢ ( ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
42	41	albii	⊢ ( ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ↔ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) )
43	36 42	anbi12i	⊢ ( ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) ↔ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
44	43	exbii	⊢ ( ∃ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) ) ↔ ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
45	33 44	sylbb	⊢ ( ∃ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ { 𝑥 ∣ 𝜑 } ) → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )
46	18 32 45	3syl	⊢ ( ∃ 𝑥 𝜑 → ∃ 𝑦 ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ∧ ∀ 𝑧 ( 𝑧 ∈ 𝑦 → ¬ ∀ 𝑥 ( 𝑥 = 𝑧 → 𝜑 ) ) ) )