Metamath Proof Explorer

Theorem permaxun

Description: The Axiom of Union ax-un holds in permutation models. Part of Exercise II.9.2 of Kunen2 p. 148. (Contributed by Eric Schmidt, 6-Nov-2025)

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

Proof

Step Hyp Ref Expression
1 permmodel.1 ⊢ 𝐹 : V –1-1-onto→ V
2 permmodel.2 ⊢ 𝑅 = ( ◡ 𝐹 ∘ E )
3 fvex ⊢ ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) ∈ V
4 breq2 ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝑧 𝑅 𝑦 ↔ 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) ) )
5 4 imbi2d ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) → ( ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 𝑦 ) ↔ ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
6 5 albidv ⊢ ( 𝑦 = ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) → ( ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 𝑦 ) ↔ ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
7 vex ⊢ 𝑧 ∈ V
8 vex ⊢ 𝑤 ∈ V
9 1 2 7 8 brpermmodel ⊢ ( 𝑧 𝑅 𝑤 ↔ 𝑧 ∈ ( 𝐹 ‘ 𝑤 ) )
10 vex ⊢ 𝑥 ∈ V
11 1 2 8 10 brpermmodel ⊢ ( 𝑤 𝑅 𝑥 ↔ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) )
12 f1ofn ⊢ ( 𝐹 : V –1-1-onto→ V → 𝐹 Fn V )
13 1 12 ax-mp ⊢ 𝐹 Fn V
14 ssv ⊢ ( 𝐹 ‘ 𝑥 ) ⊆ V
15 fnfvima ⊢ ( ( 𝐹 Fn V ∧ ( 𝐹 ‘ 𝑥 ) ⊆ V ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
16 13 14 15 mp3an12 ⊢ ( 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
17 elunii ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) → 𝑧 ∈ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
18 16 17 sylan2 ⊢ ( ( 𝑧 ∈ ( 𝐹 ‘ 𝑤 ) ∧ 𝑤 ∈ ( 𝐹 ‘ 𝑥 ) ) → 𝑧 ∈ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
19 9 11 18 syl2anb ⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 ∈ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
20 f1ofun ⊢ ( 𝐹 : V –1-1-onto→ V → Fun 𝐹 )
21 1 20 ax-mp ⊢ Fun 𝐹
22 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
23 22 funimaex ⊢ ( Fun 𝐹 → ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∈ V )
24 21 23 ax-mp ⊢ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∈ V
25 24 uniex ⊢ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ∈ V
26 1 2 7 25 brpermmodelcnv ⊢ ( 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) ↔ 𝑧 ∈ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) )
27 19 26 sylibr ⊢ ( ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) )
28 27 exlimiv ⊢ ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) )
29 28 ax-gen ⊢ ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 ( ◡ 𝐹 ‘ ∪ ( 𝐹 “ ( 𝐹 ‘ 𝑥 ) ) ) )
30 3 6 29 ceqsexv2d ⊢ ∃ 𝑦 ∀ 𝑧 ( ∃ 𝑤 ( 𝑧 𝑅 𝑤 ∧ 𝑤 𝑅 𝑥 ) → 𝑧 𝑅 𝑦 )