Theorem mnurndlem2

Description: Lemma for mnurnd . Deduction theorem input. (Contributed by Rohan Ridenour, 13-Aug-2023)

	Ref	Expression
Hypotheses	mnurndlem2.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
	mnurndlem2.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
	mnurndlem2.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
	mnurndlem2.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
	mnurndlem2.5	⊢ 𝐴 ∈ V
Assertion	mnurndlem2	⊢ ( 𝜑 → ran 𝐹 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mnurndlem2.1	⊢ 𝑀 = { 𝑘 ∣ ∀ 𝑙 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑘 ∧ ∀ 𝑚 ∃ 𝑛 ∈ 𝑘 ( 𝒫 𝑙 ⊆ 𝑛 ∧ ∀ 𝑝 ∈ 𝑙 ( ∃ 𝑞 ∈ 𝑘 ( 𝑝 ∈ 𝑞 ∧ 𝑞 ∈ 𝑚 ) → ∃ 𝑟 ∈ 𝑚 ( 𝑝 ∈ 𝑟 ∧ ∪ 𝑟 ⊆ 𝑛 ) ) ) ) }
2		mnurndlem2.2	⊢ ( 𝜑 → 𝑈 ∈ 𝑀 )
3		mnurndlem2.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑈 )
4		mnurndlem2.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
5		mnurndlem2.5	⊢ 𝐴 ∈ V
6	2	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑈 ∈ 𝑀 )
7	3	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐴 ∈ 𝑈 )
8		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
9	1 6 7 8	mnutrcld	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝑈 )
10	4	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑈 )
11	1 6 10 7	mnuprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∈ 𝑈 )
12	1 6 9 11	mnuprd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ 𝑈 )
13	12	ralrimiva	⊢ ( 𝜑 → ∀ 𝑎 ∈ 𝐴 { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ 𝑈 )
14		eqid	⊢ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) = ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } )
15	14	rnmptss	⊢ ( ∀ 𝑎 ∈ 𝐴 { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ 𝑈 → ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ⊆ 𝑈 )
16	13 15	syl	⊢ ( 𝜑 → ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ⊆ 𝑈 )
17	1 2 3 16	mnuop3d	⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑈 ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
18		simprl	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → 𝑤 ∈ 𝑈 )
19		sseq2	⊢ ( 𝑏 = 𝑤 → ( ran 𝐹 ⊆ 𝑏 ↔ ran 𝐹 ⊆ 𝑤 ) )
20	19	adantl	⊢ ( ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) ∧ 𝑏 = 𝑤 ) → ( ran 𝐹 ⊆ 𝑏 ↔ ran 𝐹 ⊆ 𝑤 ) )
21	4	adantr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → 𝐹 : 𝐴 ⟶ 𝑈 )
22		simprr	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
23	21 5 22	mnurndlem1	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ran 𝐹 ⊆ 𝑤 )
24	18 20 23	rspcedvd	⊢ ( ( 𝜑 ∧ ( 𝑤 ∈ 𝑈 ∧ ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) ) ) → ∃ 𝑏 ∈ 𝑈 ran 𝐹 ⊆ 𝑏 )
25	17 24	rexlimddv	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝑈 ran 𝐹 ⊆ 𝑏 )
26	1 2 25	mnuss2d	⊢ ( 𝜑 → ran 𝐹 ∈ 𝑈 )