Metamath Proof Explorer

Theorem permac8prim

Description: The Axiom of Choice ac8prim holds in permutation models. Part of Exercise II.9.3 of Kunen2 p. 149. Note that ax-ac requires Regularity for its derivation from the usual Axiom of Choice and does not necessarily hold in permutation models. (Contributed by Eric Schmidt, 16-Nov-2025)

Ref Expression
Hypotheses permmodel.1 ⊢ 𝐹 : V –1-1-onto→ V
permmodel.2 ⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
Assertion permac8prim ( ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ 𝐹 : V –1-1-onto→ V
2 permmodel.2 ⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3 df-ral ⊢ ( ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝐹 ‘ 𝑧 ) ≠ ∅ ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ≠ ∅ ) )
4 f1ofn ⊢ ( 𝐹 : V –1-1-onto→ V → 𝐹 Fn V )
5 1 4 ax-mp ⊢ 𝐹 Fn V
6 ssv ⊢ ( 𝐹 ‘ 𝑥 ) ⊆ V
7 neeq1 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( 𝑡 ≠ ∅ ↔ ( 𝐹 ‘ 𝑧 ) ≠ ∅ ) )
8 7 ralima ⊢ ( ( 𝐹 Fn V ∧ ( 𝐹 ‘ 𝑥 ) ⊆ V ) → ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝐹 ‘ 𝑧 ) ≠ ∅ ) )
9 5 6 8 mp2an ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝐹 ‘ 𝑧 ) ≠ ∅ )
10 vex ⊢ 𝑧 ∈ V
11 vex ⊢ 𝑥 ∈ V
12 1 2 10 11 brpermmodel ⊢ ( 𝑧 𝑅 𝑥 ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) )
13 vex ⊢ 𝑤 ∈ V
14 1 2 13 10 brpermmodel ⊢ ( 𝑤 𝑅 𝑧 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑧 ) )
15 14 exbii ⊢ ( ∃ 𝑤 𝑤 𝑅 𝑧 ↔ ∃ 𝑤 𝑤 ∈ ( 𝐹 ‘ 𝑧 ) )
16 n0 ⊢ ( ( 𝐹 ‘ 𝑧 ) ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ ( 𝐹 ‘ 𝑧 ) )
17 15 16 bitr4i ⊢ ( ∃ 𝑤 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑧 ) ≠ ∅ )
18 12 17 imbi12i ⊢ ( ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ≠ ∅ ) )
19 18 albii ⊢ ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑧 ) ≠ ∅ ) )
20 3 9 19 3bitr4i ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ↔ ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) )
21 neeq2 ⊢ ( 𝑞 = ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ≠ 𝑞 ↔ 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) ) )
22 ineq2 ⊢ ( 𝑞 = ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ 𝑞 ) = ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) )
23 22 eqeq1d ⊢ ( 𝑞 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑡 ∩ 𝑞 ) = ∅ ↔ ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
24 21 23 imbi12d ⊢ ( 𝑞 = ( 𝐹 ‘ 𝑤 ) → ( ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
25 24 ralima ⊢ ( ( 𝐹 Fn V ∧ ( 𝐹 ‘ 𝑥 ) ⊆ V ) → ( ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
26 5 6 25 mp2an ⊢ ( ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
27 26 ralbii ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
28 neeq1 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ) )
29 ineq1 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) )
30 29 eqeq1d ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ↔ ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
31 28 30 imbi12d ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
32 31 ralbidv ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ↔ ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
33 32 ralima ⊢ ( ( 𝐹 Fn V ∧ ( 𝐹 ‘ 𝑥 ) ⊆ V ) → ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
34 5 6 33 mp2an ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( 𝑡 ≠ ( 𝐹 ‘ 𝑤 ) → ( 𝑡 ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
35 r2al ⊢ ( ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∀ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
36 27 34 35 3bitri ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
37 1 2 13 11 brpermmodel ⊢ ( 𝑤 𝑅 𝑥 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
38 12 37 anbi12i ⊢ ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) )
39 df-ne ⊢ ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) ↔ ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
40 f1of1 ⊢ ( 𝐹 : V –1-1-onto→ V → 𝐹 : V –1-1→ V )
41 1 40 ax-mp ⊢ 𝐹 : V –1-1→ V
42 f1fveq ⊢ ( ( 𝐹 : V –1-1→ V ∧ ( 𝑧 ∈ V ∧ 𝑤 ∈ V ) ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
43 41 42 mpan ⊢ ( ( 𝑧 ∈ V ∧ 𝑤 ∈ V ) → ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 ) )
44 43 el2v ⊢ ( ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ 𝑧 = 𝑤 )
45 44 notbii ⊢ ( ¬ ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) ↔ ¬ 𝑧 = 𝑤 )
46 39 45 bitr2i ⊢ ( ¬ 𝑧 = 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) )
47 vex ⊢ 𝑦 ∈ V
48 1 2 47 10 brpermmodel ⊢ ( 𝑦 𝑅 𝑧 ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) )
49 1 2 47 13 brpermmodel ⊢ ( 𝑦 𝑅 𝑤 ↔ 𝑦 ∈ ( 𝐹 ‘ 𝑤 ) )
50 49 notbii ⊢ ( ¬ 𝑦 𝑅 𝑤 ↔ ¬ 𝑦 ∈ ( 𝐹 ‘ 𝑤 ) )
51 48 50 imbi12i ⊢ ( ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ↔ ( 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) → ¬ 𝑦 ∈ ( 𝐹 ‘ 𝑤 ) ) )
52 51 albii ⊢ ( ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) → ¬ 𝑦 ∈ ( 𝐹 ‘ 𝑤 ) ) )
53 disj1 ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ↔ ∀ 𝑦 ( 𝑦 ∈ ( 𝐹 ‘ 𝑧 ) → ¬ 𝑦 ∈ ( 𝐹 ‘ 𝑤 ) ) )
54 52 53 bitr4i ⊢ ( ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ↔ ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ )
55 46 54 imbi12i ⊢ ( ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ↔ ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
56 38 55 imbi12i ⊢ ( ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) ↔ ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
57 56 2albii ⊢ ( ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑧 ) ≠ ( 𝐹 ‘ 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) ) )
58 36 57 bitr4i ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) )
59 f1ofun ⊢ ( 𝐹 : V –1-1-onto→ V → Fun 𝐹 )
60 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
61 60 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∈ V )
62 1 59 61 mp2b ⊢ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∈ V
63 raleq ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑡 ∈ 𝑟 𝑡 ≠ ∅ ↔ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ) )
64 raleq ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑞 ∈ 𝑟 ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) )
65 64 raleqbi1dv ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑡 ∈ 𝑟 ∀ 𝑞 ∈ 𝑟 ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ↔ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) )
66 63 65 anbi12d ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ( ∀ 𝑡 ∈ 𝑟 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝑟 ∀ 𝑞 ∈ 𝑟 ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) ↔ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) ) )
67 raleq ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ∀ 𝑡 ∈ 𝑟 ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ) )
68 67 exbidv ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ∃ 𝑠 ∀ 𝑡 ∈ 𝑟 ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∃ 𝑠 ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ) )
69 66 68 imbi12d ⊢ ( 𝑟 = ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) → ( ( ( ∀ 𝑡 ∈ 𝑟 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝑟 ∀ 𝑞 ∈ 𝑟 ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) → ∃ 𝑠 ∀ 𝑡 ∈ 𝑟 ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ) ↔ ( ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) → ∃ 𝑠 ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ) ) )
70 ac8 ⊢ ( ( ∀ 𝑡 ∈ 𝑟 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ 𝑟 ∀ 𝑞 ∈ 𝑟 ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) → ∃ 𝑠 ∀ 𝑡 ∈ 𝑟 ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) )
71 62 69 70 vtocl ⊢ ( ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) 𝑡 ≠ ∅ ∧ ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∀ 𝑞 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ( 𝑡 ≠ 𝑞 → ( 𝑡 ∩ 𝑞 ) = ∅ ) ) → ∃ 𝑠 ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) )
72 20 58 71 syl2anbr ⊢ ( ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) ) → ∃ 𝑠 ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) )
73 ineq1 ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( 𝑡 ∩ 𝑠 ) = ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) )
74 73 eleq2d ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
75 74 eubidv ⊢ ( 𝑡 = ( 𝐹 ‘ 𝑧 ) → ( ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
76 75 ralima ⊢ ( ( 𝐹 Fn V ∧ ( 𝐹 ‘ 𝑥 ) ⊆ V ) → ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
77 5 6 76 mp2an ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) )
78 df-ral ⊢ ( ∀ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
79 77 78 bitri ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
80 fvex ⊢ ( ◡ 𝐹 ‘ 𝑠 ) ∈ V
81 12 a1i ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( 𝑧 𝑅 𝑥 ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) ) )
82 vex ⊢ 𝑣 ∈ V
83 1 2 82 10 brpermmodel ⊢ ( 𝑣 𝑅 𝑧 ↔ 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) )
84 83 a1i ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( 𝑣 𝑅 𝑧 ↔ 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ) )
85 breq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( 𝑣 𝑅 𝑦 ↔ 𝑣 𝑅 ( ◡ 𝐹 ‘ 𝑠 ) ) )
86 vex ⊢ 𝑠 ∈ V
87 1 2 82 86 brpermmodelcnv ⊢ ( 𝑣 𝑅 ( ◡ 𝐹 ‘ 𝑠 ) ↔ 𝑣 ∈ 𝑠 )
88 85 87 bitrdi ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( 𝑣 𝑅 𝑦 ↔ 𝑣 ∈ 𝑠 ) )
89 84 88 anbi12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ) )
90 89 bibi1d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ↔ ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ 𝑣 = 𝑤 ) ) )
91 90 albidv ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ↔ ∀ 𝑣 ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ 𝑣 = 𝑤 ) ) )
92 91 exbidv ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ↔ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ 𝑣 = 𝑤 ) ) )
93 elin ⊢ ( 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ↔ ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) )
94 93 eubii ⊢ ( ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ↔ ∃! 𝑣 ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) )
95 eu6 ⊢ ( ∃! 𝑣 ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ 𝑣 = 𝑤 ) )
96 94 95 bitri ⊢ ( ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ↔ ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 ∈ ( 𝐹 ‘ 𝑧 ) ∧ 𝑣 ∈ 𝑠 ) ↔ 𝑣 = 𝑤 ) )
97 92 96 bitr4di ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ↔ ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) )
98 81 97 imbi12d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ↔ ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) ) )
99 98 albidv ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ 𝑠 ) → ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) ↔ ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) ) )
100 80 99 spcev ⊢ ( ∀ 𝑧 ( 𝑧 ∈ ( 𝐹 ‘ 𝑥 ) → ∃! 𝑣 𝑣 ∈ ( ( 𝐹 ‘ 𝑧 ) ∩ 𝑠 ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
101 79 100 sylbi ⊢ ( ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
102 101 exlimiv ⊢ ( ∃ 𝑠 ∀ 𝑡 ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∃! 𝑣 𝑣 ∈ ( 𝑡 ∩ 𝑠 ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )
103 72 102 syl ⊢ ( ( ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 𝑤 𝑅 𝑧 ) ∧ ∀ 𝑧 ∀ 𝑤 ( ( 𝑧 𝑅 𝑥 ∧ 𝑤 𝑅 𝑥 ) → ( ¬ 𝑧 = 𝑤 → ∀ 𝑦 ( 𝑦 𝑅 𝑧 → ¬ 𝑦 𝑅 𝑤 ) ) ) ) → ∃ 𝑦 ∀ 𝑧 ( 𝑧 𝑅 𝑥 → ∃ 𝑤 ∀ 𝑣 ( ( 𝑣 𝑅 𝑧 ∧ 𝑣 𝑅 𝑦 ) ↔ 𝑣 = 𝑤 ) ) )