This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfac2b

Description: Axiom of Choice (first form) of Enderton p. 49 implies our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq and preleq that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a .) (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

Ref Expression
Assertion dfac2b ( CHOICE → ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )

Proof

Step Hyp Ref Expression
1 dfac3 ⊢ ( CHOICE ↔ ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
2 nfra1 ⊢ Ⅎ 𝑧 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 )
3 rsp ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) )
4 equid ⊢ 𝑧 = 𝑧
5 neeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 ≠ ∅ ↔ 𝑧 ≠ ∅ ) )
6 eqeq1 ⊢ ( 𝑢 = 𝑧 → ( 𝑢 = 𝑧 ↔ 𝑧 = 𝑧 ) )
7 5 6 anbi12d ⊢ ( 𝑢 = 𝑧 → ( ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) ↔ ( 𝑧 ≠ ∅ ∧ 𝑧 = 𝑧 ) ) )
8 7 rspcev ⊢ ( ( 𝑧 ∈ 𝑥 ∧ ( 𝑧 ≠ ∅ ∧ 𝑧 = 𝑧 ) ) → ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) )
9 4 8 mpanr2 ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) )
10 fveq2 ⊢ ( 𝑢 = 𝑧 → ( 𝑓 ‘ 𝑢 ) = ( 𝑓 ‘ 𝑧 ) )
11 10 preq1d ⊢ ( 𝑢 = 𝑧 → { ( 𝑓 ‘ 𝑢 ) , 𝑢 } = { ( 𝑓 ‘ 𝑧 ) , 𝑢 } )
12 preq2 ⊢ ( 𝑢 = 𝑧 → { ( 𝑓 ‘ 𝑧 ) , 𝑢 } = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } )
13 11 12 eqtr2d ⊢ ( 𝑢 = 𝑧 → { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } )
14 13 anim2i ⊢ ( ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) → ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
15 14 reximi ⊢ ( ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑢 = 𝑧 ) → ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
16 9 15 syl ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
17 prex ⊢ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∈ V
18 eqeq1 ⊢ ( 𝑔 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
19 18 anbi2d ⊢ ( 𝑔 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
20 19 rexbidv ⊢ ( 𝑔 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
21 17 20 elab ⊢ ( { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ↔ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
22 16 21 sylibr ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } )
23 vex ⊢ 𝑧 ∈ V
24 23 prid2 ⊢ 𝑧 ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 }
25 fvex ⊢ ( 𝑓 ‘ 𝑧 ) ∈ V
26 25 prid1 ⊢ ( 𝑓 ‘ 𝑧 ) ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 }
27 24 26 pm3.2i ⊢ ( 𝑧 ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∧ ( 𝑓 ‘ 𝑧 ) ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } )
28 eleq2 ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ) )
29 eleq2 ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ↔ ( 𝑓 ‘ 𝑧 ) ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ) )
30 28 29 anbi12d ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑧 ) , 𝑧 } → ( ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) ↔ ( 𝑧 ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∧ ( 𝑓 ‘ 𝑧 ) ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ) ) )
31 30 rspcev ⊢ ( ( { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ∧ ( 𝑧 ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ∧ ( 𝑓 ‘ 𝑧 ) ∈ { ( 𝑓 ‘ 𝑧 ) , 𝑧 } ) ) → ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) )
32 22 27 31 sylancl ⊢ ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) )
33 eleq1 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( 𝑤 ∈ 𝑧 ↔ ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) )
34 eleq1 ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( 𝑤 ∈ 𝑣 ↔ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) )
35 34 anbi2d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) ) )
36 35 rexbidv ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) ) )
37 33 36 anbi12d ⊢ ( 𝑤 = ( 𝑓 ‘ 𝑧 ) → ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) ) ) )
38 25 37 spcev ⊢ ( ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ ( 𝑓 ‘ 𝑧 ) ∈ 𝑣 ) ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
39 32 38 sylan2 ⊢ ( ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ∧ ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
40 39 ex ⊢ ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
41 3 40 syl8 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) ) ) )
42 41 impd ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) ) )
43 42 pm2.43d ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
44 df-rex ⊢ ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
45 vex ⊢ 𝑣 ∈ V
46 eqeq1 ⊢ ( 𝑔 = 𝑣 → ( 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
47 46 anbi2d ⊢ ( 𝑔 = 𝑣 → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
48 47 rexbidv ⊢ ( 𝑔 = 𝑣 → ( ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
49 45 48 elab ⊢ ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ↔ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
50 neeq1 ⊢ ( 𝑧 = 𝑢 → ( 𝑧 ≠ ∅ ↔ 𝑢 ≠ ∅ ) )
51 fveq2 ⊢ ( 𝑧 = 𝑢 → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑢 ) )
52 51 eleq1d ⊢ ( 𝑧 = 𝑢 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ 𝑢 ) ∈ 𝑧 ) )
53 eleq2 ⊢ ( 𝑧 = 𝑢 → ( ( 𝑓 ‘ 𝑢 ) ∈ 𝑧 ↔ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) )
54 52 53 bitrd ⊢ ( 𝑧 = 𝑢 → ( ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ↔ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) )
55 50 54 imbi12d ⊢ ( 𝑧 = 𝑢 → ( ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ↔ ( 𝑢 ≠ ∅ → ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ) )
56 55 rspccv ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑢 ∈ 𝑥 → ( 𝑢 ≠ ∅ → ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ) )
57 elneq ⊢ ( 𝑤 ∈ 𝑧 → 𝑤 ≠ 𝑧 )
58 57 neneqd ⊢ ( 𝑤 ∈ 𝑧 → ¬ 𝑤 = 𝑧 )
59 vex ⊢ 𝑤 ∈ V
60 neqne ⊢ ( ¬ 𝑤 = 𝑧 → 𝑤 ≠ 𝑧 )
61 prel12g ⊢ ( ( 𝑤 ∈ V ∧ 𝑧 ∈ V ∧ 𝑤 ≠ 𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ ( 𝑤 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
62 59 23 60 61 mp3an12i ⊢ ( ¬ 𝑤 = 𝑧 → ( { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ ( 𝑤 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
63 eleq2 ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( 𝑤 ∈ 𝑣 ↔ 𝑤 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
64 eleq2 ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( 𝑧 ∈ 𝑣 ↔ 𝑧 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) )
65 63 64 anbi12d ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) ↔ ( 𝑤 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ) )
66 ancom ⊢ ( ( 𝑤 ∈ 𝑣 ∧ 𝑧 ∈ 𝑣 ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) )
67 65 66 bitr3di ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑤 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ 𝑧 ∈ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
68 62 67 sylan9bbr ⊢ ( ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ ¬ 𝑤 = 𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
69 58 68 sylan2 ⊢ ( ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ 𝑤 ∈ 𝑧 ) → ( { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
70 69 adantrr ⊢ ( ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∧ ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ) → ( { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ↔ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
71 70 pm5.32da ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ∧ { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) ↔ ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
72 23 preleq ⊢ ( ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ∧ { 𝑤 , 𝑧 } = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → ( 𝑤 = ( 𝑓 ‘ 𝑢 ) ∧ 𝑧 = 𝑢 ) )
73 71 72 biimtrrdi ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ( 𝑤 = ( 𝑓 ‘ 𝑢 ) ∧ 𝑧 = 𝑢 ) ) )
74 51 eqeq2d ⊢ ( 𝑧 = 𝑢 → ( 𝑤 = ( 𝑓 ‘ 𝑧 ) ↔ 𝑤 = ( 𝑓 ‘ 𝑢 ) ) )
75 74 biimparc ⊢ ( ( 𝑤 = ( 𝑓 ‘ 𝑢 ) ∧ 𝑧 = 𝑢 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) )
76 73 75 syl6 ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( ( 𝑤 ∈ 𝑧 ∧ ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 ) ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
77 76 exp4c ⊢ ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( 𝑤 ∈ 𝑧 → ( ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
78 77 com13 ⊢ ( ( 𝑓 ‘ 𝑢 ) ∈ 𝑢 → ( 𝑤 ∈ 𝑧 → ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
79 56 78 syl8 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑢 ∈ 𝑥 → ( 𝑢 ≠ ∅ → ( 𝑤 ∈ 𝑧 → ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) ) ) )
80 79 com4r ⊢ ( 𝑤 ∈ 𝑧 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑢 ∈ 𝑥 → ( 𝑢 ≠ ∅ → ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) ) ) )
81 80 imp ⊢ ( ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑢 ∈ 𝑥 → ( 𝑢 ≠ ∅ → ( 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) ) )
82 81 imp4a ⊢ ( ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( 𝑢 ∈ 𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
83 82 com3l ⊢ ( 𝑢 ∈ 𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → ( ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
84 83 rexlimiv ⊢ ( ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑣 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → ( ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) )
85 49 84 sylbi ⊢ ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ( 𝑤 ∈ 𝑧 ∧ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) )
86 85 expd ⊢ ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( 𝑤 ∈ 𝑧 → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
87 86 com13 ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑤 ∈ 𝑧 → ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) ) ) )
88 87 imp4b ⊢ ( ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ 𝑧 ) → ( ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
89 88 exlimdv ⊢ ( ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ 𝑧 ) → ( ∃ 𝑣 ( 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ∧ ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
90 44 89 biimtrid ⊢ ( ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) ∧ 𝑤 ∈ 𝑧 ) → ( ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
91 90 expimpd ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
92 91 alrimiv ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑤 ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) )
93 mo2icl ⊢ ( ∀ 𝑤 ( ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → 𝑤 = ( 𝑓 ‘ 𝑧 ) ) → ∃* 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
94 92 93 syl ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃* 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
95 43 94 jctird ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) ) )
96 df-reu ⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃! 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
97 df-eu ⊢ ( ∃! 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
98 96 97 bitri ⊢ ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ( ∃ 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ∧ ∃* 𝑤 ( 𝑤 ∈ 𝑧 ∧ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
99 95 98 imbitrrdi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( ( 𝑧 ∈ 𝑥 ∧ 𝑧 ≠ ∅ ) → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
100 99 expd ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ( 𝑧 ∈ 𝑥 → ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
101 2 100 ralrimi ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
102 vex ⊢ 𝑓 ∈ V
103 102 rnex ⊢ ran 𝑓 ∈ V
104 p0ex ⊢ { ∅ } ∈ V
105 103 104 unex ⊢ ( ran 𝑓 ∪ { ∅ } ) ∈ V
106 vex ⊢ 𝑥 ∈ V
107 105 106 unex ⊢ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∈ V
108 107 pwex ⊢ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∈ V
109 ssun1 ⊢ ( ran 𝑓 ∪ { ∅ } ) ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
110 fvrn0 ⊢ ( 𝑓 ‘ 𝑢 ) ∈ ( ran 𝑓 ∪ { ∅ } )
111 109 110 sselii ⊢ ( 𝑓 ‘ 𝑢 ) ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
112 elun2 ⊢ ( 𝑢 ∈ 𝑥 → 𝑢 ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
113 prssi ⊢ ( ( ( 𝑓 ‘ 𝑢 ) ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ∧ 𝑢 ∈ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) → { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
114 111 112 113 sylancr ⊢ ( 𝑢 ∈ 𝑥 → { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
115 prex ⊢ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∈ V
116 115 elpw ⊢ ( { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ↔ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ⊆ ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
117 114 116 sylibr ⊢ ( 𝑢 ∈ 𝑥 → { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
118 eleq1 ⊢ ( 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → ( 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ↔ { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
119 117 118 syl5ibrcom ⊢ ( 𝑢 ∈ 𝑥 → ( 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
120 119 adantld ⊢ ( 𝑢 ∈ 𝑥 → ( ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) ) )
121 120 rexlimiv ⊢ ( ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) → 𝑔 ∈ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 ) )
122 121 abssi ⊢ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ⊆ 𝒫 ( ( ran 𝑓 ∪ { ∅ } ) ∪ 𝑥 )
123 108 122 ssexi ⊢ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ∈ V
124 rexeq ⊢ ( 𝑦 = { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
125 124 reubidv ⊢ ( 𝑦 = { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ↔ ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
126 125 imbi2d ⊢ ( 𝑦 = { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
127 126 ralbidv ⊢ ( 𝑦 = { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } → ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ↔ ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) ) )
128 123 127 spcev ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ { 𝑔 ∣ ∃ 𝑢 ∈ 𝑥 ( 𝑢 ≠ ∅ ∧ 𝑔 = { ( 𝑓 ‘ 𝑢 ) , 𝑢 } ) } ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
129 101 128 syl ⊢ ( ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
130 129 exlimiv ⊢ ( ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
131 130 alimi ⊢ ( ∀ 𝑥 ∃ 𝑓 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑓 ‘ 𝑧 ) ∈ 𝑧 ) → ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )
132 1 131 sylbi ⊢ ( CHOICE → ∀ 𝑥 ∃ 𝑦 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ∃! 𝑤 ∈ 𝑧 ∃ 𝑣 ∈ 𝑦 ( 𝑧 ∈ 𝑣 ∧ 𝑤 ∈ 𝑣 ) ) )