Metamath Proof Explorer

Theorem permaxinf2lem

Description: Lemma for permaxinf2 . (Contributed by Eric Schmidt, 6-Nov-2025)

Ref Expression
Hypotheses permmodel.1 ⊢ 𝐹 : V –1-1-onto→ V
permmodel.2 ⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
permaxinf2lem.3 ⊢ 𝑍 = ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω )
Assertion permaxinf2lem ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ 𝐹 : V –1-1-onto→ V
2 permmodel.2 ⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3 permaxinf2lem.3 ⊢ 𝑍 = ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω )
4 fvex ⊢ ( ◡ 𝐹 ‘ 𝑍 ) ∈ V
5 breq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( 𝑦 𝑅 𝑥 ↔ 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ) )
6 5 anbi1d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ↔ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ) )
7 6 exbidv ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ↔ ∃ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ) )
8 breq2 ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( 𝑧 𝑅 𝑥 ↔ 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ) )
9 8 anbi1d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ↔ ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
10 9 exbidv ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ↔ ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
11 5 10 imbi12d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ↔ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
12 11 albidv ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ↔ ∀ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) )
13 7 12 anbi12d ⊢ ( 𝑥 = ( ◡ 𝐹 ‘ 𝑍 ) → ( ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) ↔ ( ∃ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) ) ) )
14 fvex ⊢ ( ◡ 𝐹 ‘ ∅ ) ∈ V
15 breq1 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∅ ) → ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ↔ ( ◡ 𝐹 ‘ ∅ ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ) )
16 breq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∅ ) → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
17 16 notbid ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∅ ) → ( ¬ 𝑧 𝑅 𝑦 ↔ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
18 17 albidv ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∅ ) → ( ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ↔ ∀ 𝑧 ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) )
19 15 18 anbi12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∅ ) → ( ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ↔ ( ( ◡ 𝐹 ‘ ∅ ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) ) ) )
20 orbitinit ⊢ ( ( ◡ 𝐹 ‘ ∅ ) ∈ V → ( ◡ 𝐹 ‘ ∅ ) ∈ ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω ) )
21 20 3 eleqtrrdi ⊢ ( ( ◡ 𝐹 ‘ ∅ ) ∈ V → ( ◡ 𝐹 ‘ ∅ ) ∈ 𝑍 )
22 14 21 ax-mp ⊢ ( ◡ 𝐹 ‘ ∅ ) ∈ 𝑍
23 orbitex ⊢ ( rec ( ( 𝑣 ∈ V ↦ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) ) , ( ◡ 𝐹 ‘ ∅ ) ) “ ω ) ∈ V
24 3 23 eqeltri ⊢ 𝑍 ∈ V
25 1 2 14 24 brpermmodelcnv ⊢ ( ( ◡ 𝐹 ‘ ∅ ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ↔ ( ◡ 𝐹 ‘ ∅ ) ∈ 𝑍 )
26 22 25 mpbir ⊢ ( ◡ 𝐹 ‘ ∅ ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 )
27 noel ⊢ ¬ 𝑧 ∈ ∅
28 vex ⊢ 𝑧 ∈ V
29 0ex ⊢ ∅ ∈ V
30 1 2 28 29 brpermmodelcnv ⊢ ( 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) ↔ 𝑧 ∈ ∅ )
31 27 30 mtbir ⊢ ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ )
32 31 ax-gen ⊢ ∀ 𝑧 ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ )
33 26 32 pm3.2i ⊢ ( ( ◡ 𝐹 ‘ ∅ ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∅ ) )
34 14 19 33 ceqsexv2d ⊢ ∃ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 )
35 fvex ⊢ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ∈ V
36 nfcv ⊢ Ⅎ 𝑣 𝑦
37 nfcv ⊢ Ⅎ 𝑣 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) )
38 fveq2 ⊢ ( 𝑣 = 𝑦 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝑦 ) )
39 sneq ⊢ ( 𝑣 = 𝑦 → { 𝑣 } = { 𝑦 } )
40 38 39 uneq12d ⊢ ( 𝑣 = 𝑦 → ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) = ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) )
41 40 fveq2d ⊢ ( 𝑣 = 𝑦 → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑣 ) ∪ { 𝑣 } ) ) = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) )
42 36 37 3 41 orbitclmpt ⊢ ( ( 𝑦 ∈ 𝑍 ∧ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ∈ V ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ∈ 𝑍 )
43 35 42 mpan2 ⊢ ( 𝑦 ∈ 𝑍 → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ∈ 𝑍 )
44 vex ⊢ 𝑦 ∈ V
45 1 2 44 24 brpermmodelcnv ⊢ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ↔ 𝑦 ∈ 𝑍 )
46 1 2 35 24 brpermmodelcnv ⊢ ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ∈ 𝑍 )
47 43 45 46 3imtr4i ⊢ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) )
48 vex ⊢ 𝑤 ∈ V
49 fvex ⊢ ( 𝐹 ‘ 𝑦 ) ∈ V
50 vsnex ⊢ { 𝑦 } ∈ V
51 49 50 unex ⊢ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ∈ V
52 1 2 48 51 brpermmodelcnv ⊢ ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ 𝑤 ∈ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) )
53 elun ⊢ ( 𝑤 ∈ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ↔ ( 𝑤 ∈ ( 𝐹 ‘ 𝑦 ) ∨ 𝑤 ∈ { 𝑦 } ) )
54 1 2 48 44 brpermmodel ⊢ ( 𝑤 𝑅 𝑦 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑦 ) )
55 54 bicomi ⊢ ( 𝑤 ∈ ( 𝐹 ‘ 𝑦 ) ↔ 𝑤 𝑅 𝑦 )
56 velsn ⊢ ( 𝑤 ∈ { 𝑦 } ↔ 𝑤 = 𝑦 )
57 55 56 orbi12i ⊢ ( ( 𝑤 ∈ ( 𝐹 ‘ 𝑦 ) ∨ 𝑤 ∈ { 𝑦 } ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) )
58 52 53 57 3bitri ⊢ ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) )
59 58 ax-gen ⊢ ∀ 𝑤 ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) )
60 breq1 ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) → ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ↔ ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ) )
61 breq2 ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) → ( 𝑤 𝑅 𝑧 ↔ 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ) )
62 61 bibi1d ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) → ( ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ↔ ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
63 62 albidv ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) → ( ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ↔ ∀ 𝑤 ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
64 60 63 anbi12d ⊢ ( 𝑧 = ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) → ( ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ↔ ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
65 35 64 spcev ⊢ ( ( ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 ( ◡ 𝐹 ‘ ( ( 𝐹 ‘ 𝑦 ) ∪ { 𝑦 } ) ) ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
66 47 59 65 sylancl ⊢ ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
67 66 ax-gen ⊢ ∀ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) )
68 34 67 pm3.2i ⊢ ( ∃ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) → ∃ 𝑧 ( 𝑧 𝑅 ( ◡ 𝐹 ‘ 𝑍 ) ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )
69 4 13 68 ceqsexv2d ⊢ ∃ 𝑥 ( ∃ 𝑦 ( 𝑦 𝑅 𝑥 ∧ ∀ 𝑧 ¬ 𝑧 𝑅 𝑦 ) ∧ ∀ 𝑦 ( 𝑦 𝑅 𝑥 → ∃ 𝑧 ( 𝑧 𝑅 𝑥 ∧ ∀ 𝑤 ( 𝑤 𝑅 𝑧 ↔ ( 𝑤 𝑅 𝑦 ∨ 𝑤 = 𝑦 ) ) ) ) )