Metamath Proof Explorer

Theorem mnurndlem1

Description: Lemma for mnurnd . (Contributed by Rohan Ridenour, 12-Aug-2023)

Ref Expression
Hypotheses mnurndlem1.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
mnurndlem1.4 ⊢ 𝐴 ∈ V
mnurndlem1.6 ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
Assertion mnurndlem1 ( 𝜑 → ran 𝐹 ⊆ 𝑤 )

Proof

Step Hyp Ref Expression
1 mnurndlem1.3 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝑈 )
2 mnurndlem1.4 ⊢ 𝐴 ∈ V
3 mnurndlem1.6 ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
4 1 ffnd ⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
5 vex ⊢ 𝑖 ∈ V
6 5 prid1 ⊢ 𝑖 ∈ { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } }
7 simpr ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑣 = { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } ) → 𝑣 = { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } )
8 6 7 eleqtrrid ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑣 = { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } ) → 𝑖 ∈ 𝑣 )
9 eqid ⊢ ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) = ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } )
10 id ⊢ ( 𝑖 ∈ 𝐴 → 𝑖 ∈ 𝐴 )
11 prex ⊢ { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } ∈ V
12 11 a1i ⊢ ( 𝑖 ∈ 𝐴 → { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } ∈ V )
13 id ⊢ ( 𝑎 = 𝑖 → 𝑎 = 𝑖 )
14 fveq2 ⊢ ( 𝑎 = 𝑖 → ( 𝐹 ‘ 𝑎 ) = ( 𝐹 ‘ 𝑖 ) )
15 14 preq1d ⊢ ( 𝑎 = 𝑖 → { ( 𝐹 ‘ 𝑎 ) , 𝐴 } = { ( 𝐹 ‘ 𝑖 ) , 𝐴 } )
16 13 15 preq12d ⊢ ( 𝑎 = 𝑖 → { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } = { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } )
17 16 adantl ⊢ ( ( 𝑖 ∈ 𝐴 ∧ 𝑎 = 𝑖 ) → { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } = { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } )
18 9 10 12 17 rr-elrnmpt3d ⊢ ( 𝑖 ∈ 𝐴 → { 𝑖 , { ( 𝐹 ‘ 𝑖 ) , 𝐴 } } ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) )
19 8 18 rspcime ⊢ ( 𝑖 ∈ 𝐴 → ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 )
20 19 rgen ⊢ ∀ 𝑖 ∈ 𝐴 ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣
21 ralim ⊢ ( ∀ 𝑖 ∈ 𝐴 ( ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) → ( ∀ 𝑖 ∈ 𝐴 ∃ 𝑣 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) 𝑖 ∈ 𝑣 → ∀ 𝑖 ∈ 𝐴 ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ) )
22 3 20 21 mpisyl ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) )
23 prex ⊢ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ V
24 23 rgenw ⊢ ∀ 𝑎 ∈ 𝐴 { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ V
25 eleq2 ⊢ ( 𝑢 = { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( 𝑖 ∈ 𝑢 ↔ 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) )
26 unieq ⊢ ( 𝑢 = { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ∪ 𝑢 = ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } )
27 26 sseq1d ⊢ ( 𝑢 = { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( ∪ 𝑢 ⊆ 𝑤 ↔ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) )
28 25 27 anbi12d ⊢ ( 𝑢 = { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) )
29 9 28 rexrnmptw ⊢ ( ∀ 𝑎 ∈ 𝐴 { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∈ V → ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑎 ∈ 𝐴 ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) )
30 24 29 ax-mp ⊢ ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) ↔ ∃ 𝑎 ∈ 𝐴 ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) )
31 simplrl ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } )
32 simpr ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → 𝑖 ∈ 𝐴 )
33 2 prid2 ⊢ 𝐴 ∈ { ( 𝐹 ‘ 𝑎 ) , 𝐴 }
34 elnotel ⊢ ( 𝐴 ∈ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } → ¬ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∈ 𝐴 )
35 33 34 ax-mp ⊢ ¬ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∈ 𝐴
36 35 a1i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ¬ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∈ 𝐴 )
37 32 36 elnelneq2d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ¬ 𝑖 = { ( 𝐹 ‘ 𝑎 ) , 𝐴 } )
38 elpri ⊢ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( 𝑖 = 𝑎 ∨ 𝑖 = { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ) )
39 38 orcomd ⊢ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( 𝑖 = { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∨ 𝑖 = 𝑎 ) )
40 39 ord ⊢ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } → ( ¬ 𝑖 = { ( 𝐹 ‘ 𝑎 ) , 𝐴 } → 𝑖 = 𝑎 ) )
41 31 37 40 sylc ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → 𝑖 = 𝑎 )
42 41 fveq2d ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑖 ) = ( 𝐹 ‘ 𝑎 ) )
43 simplrr ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 )
44 vex ⊢ 𝑎 ∈ V
45 prex ⊢ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ∈ V
46 44 45 unipr ⊢ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } = ( 𝑎 ∪ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } )
47 46 sseq1i ⊢ ( ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ↔ ( 𝑎 ∪ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ) ⊆ 𝑤 )
48 unss ⊢ ( ( 𝑎 ⊆ 𝑤 ∧ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 ) ↔ ( 𝑎 ∪ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ) ⊆ 𝑤 )
49 48 bicomi ⊢ ( ( 𝑎 ∪ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ) ⊆ 𝑤 ↔ ( 𝑎 ⊆ 𝑤 ∧ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 ) )
50 49 simprbi ⊢ ( ( 𝑎 ∪ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ) ⊆ 𝑤 → { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 )
51 47 50 sylbi ⊢ ( ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 → { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 )
52 fvex ⊢ ( 𝐹 ‘ 𝑎 ) ∈ V
53 52 2 prss ⊢ ( ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤 ) ↔ { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 )
54 53 bicomi ⊢ ( { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 ↔ ( ( 𝐹 ‘ 𝑎 ) ∈ 𝑤 ∧ 𝐴 ∈ 𝑤 ) )
55 54 simplbi ⊢ ( { ( 𝐹 ‘ 𝑎 ) , 𝐴 } ⊆ 𝑤 → ( 𝐹 ‘ 𝑎 ) ∈ 𝑤 )
56 43 51 55 3syl ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑎 ) ∈ 𝑤 )
57 42 56 eqeltrd ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) ∧ 𝑖 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 )
58 57 ex ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) ) → ( 𝑖 ∈ 𝐴 → ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 ) )
59 58 rexlimiva ⊢ ( ∃ 𝑎 ∈ 𝐴 ( 𝑖 ∈ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ∧ ∪ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ⊆ 𝑤 ) → ( 𝑖 ∈ 𝐴 → ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 ) )
60 30 59 sylbi ⊢ ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) → ( 𝑖 ∈ 𝐴 → ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 ) )
61 60 com12 ⊢ ( 𝑖 ∈ 𝐴 → ( ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) → ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 ) )
62 61 ralimia ⊢ ( ∀ 𝑖 ∈ 𝐴 ∃ 𝑢 ∈ ran ( 𝑎 ∈ 𝐴 ↦ { 𝑎 , { ( 𝐹 ‘ 𝑎 ) , 𝐴 } } ) ( 𝑖 ∈ 𝑢 ∧ ∪ 𝑢 ⊆ 𝑤 ) → ∀ 𝑖 ∈ 𝐴 ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 )
63 22 62 syl ⊢ ( 𝜑 → ∀ 𝑖 ∈ 𝐴 ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 )
64 fnfvrnss ⊢ ( ( 𝐹 Fn 𝐴 ∧ ∀ 𝑖 ∈ 𝐴 ( 𝐹 ‘ 𝑖 ) ∈ 𝑤 ) → ran 𝐹 ⊆ 𝑤 )
65 4 63 64 syl2anc ⊢ ( 𝜑 → ran 𝐹 ⊆ 𝑤 )