P. 457 of Theorem List - Metamath Proof Explorer

Type

Label

Description

Statement

Theorem

2sb5ndVD 45601*

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2sb5nd 45252 is 2sb5ndVD 45601 without virtual deductions and was automatically derived from 2sb5ndVD 45601. (Contributed by Alan Sare, 30-Apr-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑) ↔ ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
2:1:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
3::	⊢ ([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
4:3:	⊢ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 → ∀𝑦[𝑣 / 𝑦]𝜑)
5:4:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → [𝑢 / 𝑥] ∀𝑦[𝑣 / 𝑦]𝜑)
6::	⊢ (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ¬ ∀𝑥𝑥 = 𝑦   )
7::	⊢ (∀𝑦𝑦 = 𝑥 → ∀𝑥𝑥 = 𝑦)
8:7:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ¬ ∀𝑦𝑦 = 𝑥)
9:6,8:	⊢ (   ¬ ∀𝑥𝑥 = 𝑦   ▶   ¬ ∀𝑦𝑦 = 𝑥   )
10:9:	⊢ ([𝑢 / 𝑥]∀𝑦[𝑣 / 𝑦]𝜑 ↔ ∀ 𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
11:5,10:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
12:11:	⊢ (¬ ∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
13::	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑥[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
14::	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ∀𝑥𝑥 = 𝑦   )
15:14:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   (∀𝑥[𝑢 / 𝑥][ 𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
16:13,15:	⊢ (   ∀𝑥𝑥 = 𝑦   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦 ]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)   )
17:16:	⊢ (∀𝑥𝑥 = 𝑦 → ([𝑢 / 𝑥][𝑣 / 𝑦] 𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
19:12,17:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 → ∀𝑦[𝑢 / 𝑥][𝑣 / 𝑦]𝜑)
20:19:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
21:2,20:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ (∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
22:21:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ↔ ∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
23:13:	⊢ (∃𝑥(∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
24:22,23:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
240:24:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
241::	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑)) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑))
242:241,240:	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
243::	⊢ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ( [𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))) ↔ ((∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜑) ↔ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))))
25:242,243:	⊢ (∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣) → ([ 𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))
26::	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥 ∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))
qed:25,26:	⊢ ((¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

2uasbanhVD 45602*

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. 2uasbanh 45253 is 2uasbanhVD 45602 without virtual deductions and was automatically derived from 2uasbanhVD 45602. (Contributed by Alan Sare, 31-May-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

h1::	⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
100:1:	⊢ (𝜒 → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
2:100:	⊢ (   𝜒   ▶   (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))   )
3:2:	⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   )
4:3:	⊢ (   𝜒   ▶   ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣 )   )
5:4:	⊢ (   𝜒   ▶   (¬ ∀𝑥𝑥 = 𝑦 ∨ 𝑢 = 𝑣)    )
6:5:	⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))   )
7:3,6:	⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜑   )
8:2:	⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)   )
9:5:	⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦]𝜓 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))   )
10:8,9:	⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦]𝜓   )
101::	⊢ ([𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
102:101:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ [𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦]𝜓))
103::	⊢ ([𝑢 / 𝑥]([𝑣 / 𝑦]𝜑 ∧ [𝑣 / 𝑦 ]𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
104:102,103:	⊢ ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ∧ [𝑢 / 𝑥][𝑣 / 𝑦]𝜓))
11:7,10,104:	⊢ (   𝜒   ▶   [𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓)   )
110:5:	⊢ (   𝜒   ▶   ([𝑢 / 𝑥][𝑣 / 𝑦](𝜑 ∧ 𝜓) ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))   )
12:11,110:	⊢ (   𝜒   ▶   ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))   )
120:12:	⊢ (𝜒 → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ (𝜑 ∧ 𝜓)))
13:1,120:	⊢ ((∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)))
14::	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓))   )
15:14:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   (𝑥 = 𝑢 ∧ 𝑦 = 𝑣)   )
16:14:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   (𝜑 ∧ 𝜓)   )
17:16:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   𝜑   )
18:15,17:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)   )
19:18:	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
20:19:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
21:20:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑))
22:16:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   𝜓   )
23:15,22:	⊢ (   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 ))   ▶   ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)   )
24:23:	⊢ (((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓 )) → ((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
25:24:	⊢ (∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) → ∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
26:25:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓))
27:21,26:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) → (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))
qed:13,27:	⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ ( 𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦( (𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

⊢ (𝜒 ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))    ⇒   ⊢ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ (𝜑 ∧ 𝜓)) ↔ (∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑) ∧ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜓)))

Theorem

e2ebindVD 45603

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. e2ebind 45255 is e2ebindVD 45603 without virtual deductions and was automatically derived from e2ebindVD 45603.

1::	⊢ (𝜑 ↔ 𝜑)
2:1:	⊢ (∀𝑦𝑦 = 𝑥 → (𝜑 ↔ 𝜑))
3:2:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑦𝜑 ↔ ∃𝑥𝜑 ))
4::	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   ∀𝑦𝑦 = 𝑥   )
5:3,4:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦𝜑 ↔ ∃𝑥 𝜑)   )
6::	⊢ (∀𝑦𝑦 = 𝑥 → ∀𝑦∀𝑦𝑦 = 𝑥)
7:5,6:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   ∀𝑦(∃𝑦𝜑 ↔ ∃𝑥𝜑)   )
8:7:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑦∃𝑥𝜑)   )
9::	⊢ (∃𝑦∃𝑥𝜑 ↔ ∃𝑥∃𝑦𝜑)
10:8,9:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑦∃𝑦𝜑 ↔ ∃𝑥∃𝑦𝜑)   )
11::	⊢ (∃𝑦𝜑 → ∀𝑦∃𝑦𝜑)
12:11:	⊢ (∃𝑦∃𝑦𝜑 ↔ ∃𝑦𝜑)
13:10,12:	⊢ (   ∀𝑦𝑦 = 𝑥   ▶   (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑)   )
14:13:	⊢ (∀𝑦𝑦 = 𝑥 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))
15::	⊢ (∀𝑦𝑦 = 𝑥 ↔ ∀𝑥𝑥 = 𝑦)
qed:14,15:	⊢ (∀𝑥𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃ 𝑦𝜑))

(Contributed by Alan Sare, 27-Nov-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

21.42.8  Virtual Deduction transcriptions of textbook proofs

Theorem

sb5ALTVD 45604*

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 20 Excercise 3.a., which is sb5 2311, found in the "Answers to Starred Exercises" on page 457 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sb5ALT 45217 is sb5ALTVD 45604 without virtual deductions and was automatically derived from sb5ALTVD 45604.

1::	⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥]𝜑   )
2::	⊢ [𝑦 / 𝑥]𝑥 = 𝑦
3:1,2:	⊢ (   [𝑦 / 𝑥]𝜑   ▶   [𝑦 / 𝑥](𝑥 = 𝑦 ∧ 𝜑)   )
4:3:	⊢ (   [𝑦 / 𝑥]𝜑   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 )   )
5:4:	⊢ ([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )
6::	⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ▶   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   )
7::	⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   (𝑥 = 𝑦 ∧ 𝜑)   )
8:7:	⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   𝜑   )
9:7:	⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   𝑥 = 𝑦   )
10:8,9:	⊢ (   ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)   ,   (𝑥 = 𝑦 ∧ 𝜑 )   ▶   [𝑦 / 𝑥]𝜑   )
101::	⊢ ([𝑦 / 𝑥]𝜑 → ∀𝑥[𝑦 / 𝑥]𝜑)
11:101,10:	⊢ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑 )
12:5,11:	⊢ (([𝑦 / 𝑥]𝜑 → ∃𝑥(𝑥 = 𝑦 ∧ 𝜑 )) ∧ (∃𝑥(𝑥 = 𝑦 ∧ 𝜑) → [𝑦 / 𝑥]𝜑))
qed:12:	⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑) )

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ([𝑦 / 𝑥]𝜑 ↔ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))

Theorem

vk15.4jVD 45605

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Unit 15 Excercise 4.f. found in the "Answers to Starred Exercises" on page 442 of "Understanding Symbolic Logic", Fifth Edition (2008), by Virginia Klenk. The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. vk15.4j 45220 is vk15.4jVD 45605 without virtual deductions and was automatically derived from vk15.4jVD 45605. Step numbers greater than 25 are additional steps necessary for the sequent calculus proof not contained in the Fitch-style proof. Otherwise, step i of the User's Proof corresponds to step i of the Fitch-style proof.

h1::	⊢ ¬ (∃𝑥¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))
h2::	⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏 ))
h3::	⊢ ¬ ∀𝑥(𝜏 → 𝜑)
4::	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∃𝑥¬ 𝜃   )
5:4:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∀𝑥𝜃   )
6:3:	⊢ ∃𝑥(𝜏 ∧ ¬ 𝜑)
7::	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜏 ∧ ¬ 𝜑)   )
8:7:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   𝜏   )
9:7:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ 𝜑   )
10:5:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   𝜃   )
11:10,8:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   (𝜃 ∧ 𝜏)   )
12:11:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥(𝜃 ∧ 𝜏)   )
13:12:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ ¬ ∃𝑥(𝜃 ∧ 𝜏)   )
14:2,13:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ¬ ∀𝑥𝜒   )
140::	⊢ (∃𝑥¬ 𝜃 → ∀𝑥∃𝑥¬ 𝜃 )
141:140:	⊢ (¬ ∃𝑥¬ 𝜃 → ∀𝑥¬ ∃𝑥 ¬ 𝜃)
142::	⊢ (∀𝑥𝜒 → ∀𝑥∀𝑥𝜒)
143:142:	⊢ (¬ ∀𝑥𝜒 → ∀𝑥¬ ∀𝑥𝜒 )
144:6,14,141,143:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∀𝑥𝜒    )
15:1:	⊢ (¬ ∃𝑥¬ 𝜑 ∨ ¬ ∃𝑥(𝜓 ∧ ¬ 𝜒))
16:9:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   (𝜏 ∧ ¬ 𝜑)   ▶   ∃𝑥¬ 𝜑   )
161::	⊢ (∃𝑥¬ 𝜑 → ∀𝑥∃𝑥¬ 𝜑 )
162:6,16,141,161:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜑    )
17:162:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ¬ ∃𝑥 ¬ 𝜑   )
18:15,17:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∃𝑥( 𝜓 ∧ ¬ 𝜒)   )
19:18:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∀𝑥(𝜓 → 𝜒)   )
20:144:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜒    )
21::	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ¬ 𝜒   )
22:19:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   (𝜓 → 𝜒 )   )
23:21,22:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ¬ 𝜓   )
24:23:	⊢ (   ¬ ∃𝑥¬ 𝜃   ,   ¬ 𝜒   ▶   ∃ 𝑥¬ 𝜓   )
240::	⊢ (∃𝑥¬ 𝜓 → ∀𝑥∃𝑥¬ 𝜓 )
241:20,24,141,240:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ∃𝑥¬ 𝜓    )
25:241:	⊢ (   ¬ ∃𝑥¬ 𝜃   ▶   ¬ ∀𝑥𝜓    )
qed:25:	⊢ (¬ ∃𝑥¬ 𝜃 → ¬ ∀𝑥𝜓)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ¬ (∃𝑥 ¬ 𝜑 ∧ ∃𝑥(𝜓 ∧ ¬ 𝜒))    &   ⊢ (∀𝑥𝜒 → ¬ ∃𝑥(𝜃 ∧ 𝜏))    &   ⊢ ¬ ∀𝑥(𝜏 → 𝜑)    ⇒   ⊢ (¬ ∃𝑥 ¬ 𝜃 → ¬ ∀𝑥𝜓)

Theorem

notnotrALTVD 45606

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 5 of Section 14 of [Margaris] p. 59 (which is notnotr 131). The same proof may also be interpreted as a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. notnotrALT 45221 is notnotrALTVD 45606 without virtual deductions and was automatically derived from notnotrALTVD 45606. Step i of the User's Proof corresponds to step i of the Fitch-style proof.

1::	⊢ (   ¬ ¬ 𝜑   ▶   ¬ ¬ 𝜑   )
2::	⊢ (¬ ¬ 𝜑 → (¬ 𝜑 → ¬ ¬ ¬ 𝜑))
3:1:	⊢ (   ¬ ¬ 𝜑   ▶   (¬ 𝜑 → ¬ ¬ ¬ 𝜑)   )
4::	⊢ ((¬ 𝜑 → ¬ ¬ ¬ 𝜑) → (¬ ¬ 𝜑 → 𝜑))
5:3:	⊢ (   ¬ ¬ 𝜑   ▶   (¬ ¬ 𝜑 → 𝜑)   )
6:5,1:	⊢ (   ¬ ¬ 𝜑   ▶   𝜑   )
qed:6:	⊢ (¬ ¬ 𝜑 → 𝜑)

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

con3ALTVD 45607

The following User's Proof is a Natural Deduction Sequent Calculus transcription of the Fitch-style Natural Deduction proof of Theorem 7 of Section 14 of [Margaris] p. 60 (which is con3 154). The same proof may also be interpreted to be a Virtual Deduction Hilbert-style axiomatic proof. It was completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. con3ALT2 45222 is con3ALTVD 45607 without virtual deductions and was automatically derived from con3ALTVD 45607. Step i of the User's Proof corresponds to step i of the Fitch-style proof.

1::	⊢ (   (𝜑 → 𝜓)   ▶   (𝜑 → 𝜓)   )
2::	⊢ (   (𝜑 → 𝜓)   ,   ¬ ¬ 𝜑   ▶   ¬ ¬ 𝜑   )
3::	⊢ (¬ ¬ 𝜑 → 𝜑)
4:2:	⊢ (   (𝜑 → 𝜓)   ,   ¬ ¬ 𝜑   ▶   𝜑   )
5:1,4:	⊢ (   (𝜑 → 𝜓)   ,   ¬ ¬ 𝜑   ▶   𝜓   )
6::	⊢ (𝜓 → ¬ ¬ 𝜓)
7:6,5:	⊢ (   (𝜑 → 𝜓)   ,   ¬ ¬ 𝜑   ▶   ¬ ¬ 𝜓   )
8:7:	⊢ (   (𝜑 → 𝜓)   ▶   (¬ ¬ 𝜑 → ¬ ¬ 𝜓 )   )
9::	⊢ ((¬ ¬ 𝜑 → ¬ ¬ 𝜓) → (¬ 𝜓 → ¬ 𝜑))
10:8:	⊢ (   (𝜑 → 𝜓)   ▶   (¬ 𝜓 → ¬ 𝜑)   )
qed:10:	⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

(Contributed by Alan Sare, 21-Apr-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝜑 → 𝜓) → (¬ 𝜓 → ¬ 𝜑))

21.42.9  Theorems proved using conjunction-form Virtual Deduction

Theorem

elpwgdedVD 45608

Membership in a power class. Theorem 86 of [Suppes] p. 47. Derived from elpwg 4566. In form of VD deduction with 𝜑 and 𝜓 as variable virtual hypothesis collections based on Mario Carneiro's metavariable concept. elpwgded 45256 is elpwgdedVD 45608 using conventional notation. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (   𝜑   ▶   𝐴 ∈ V   )    &   ⊢ (   𝜓   ▶   𝐴 ⊆ 𝐵   )    ⇒   ⊢ (   (   𝜑   ,   𝜓   )   ▶   𝐴 ∈ 𝒫 𝐵   )

Theorem

sspwimp 45609

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. For the biconditional, see sspwb 5432. The proof sspwimp 45609, using conventional notation, was translated from virtual deduction form, sspwimpVD 45610, using a translation program. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpVD 45610

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) using conjunction-form virtual hypothesis collections. It was completed manually, but has the potential to be completed automatically by a tools program which would invoke Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimp 45609 is sspwimpVD 45610 without virtual deductions and was derived from sspwimpVD 45610. (Contributed by Alan Sare, 23-Apr-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   .............. 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcf 45611

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpcf 45611, using conventional notation, was translated from its virtual deduction form, sspwimpcfVD 45612, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

sspwimpcfVD 45612

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) using conjunction-form virtual hypothesis collections. It was completed automatically by a tools program which would invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. sspwimpcf 45611 is sspwimpcfVD 45612 without virtual deductions and was derived from sspwimpcfVD 45612. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   𝐴 ⊆ 𝐵   ▶   𝐴 ⊆ 𝐵   )
2::	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ∈ 𝒫 𝐴   )
3:2:	⊢ (   ........... 𝑥 ∈ 𝒫 𝐴    ▶   𝑥 ⊆ 𝐴   )
4:3,1:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ⊆ 𝐵   )
5::	⊢ 𝑥 ∈ V
6:4,5:	⊢ (   (   𝐴 ⊆ 𝐵   ,   𝑥 ∈ 𝒫 𝐴   )   ▶   𝑥 ∈ 𝒫 𝐵    )
7:6:	⊢ (   𝐴 ⊆ 𝐵   ▶   (𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)    )
8:7:	⊢ (   𝐴 ⊆ 𝐵   ▶   ∀𝑥(𝑥 ∈ 𝒫 𝐴 → 𝑥 ∈ 𝒫 𝐵)   )
9:8:	⊢ (   𝐴 ⊆ 𝐵   ▶   𝒫 𝐴 ⊆ 𝒫 𝐵   )
qed:9:	⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

suctrALTcf 45613

The successor of a transitive class is transitive. suctrALTcf 45613, using conventional notation, was translated from virtual deduction form, suctrALTcfVD 45614, using a translation program. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

suctrALTcfVD 45614

The following User's Proof is a Virtual Deduction proof (see wvd1 45261) using conjunction-form virtual hypothesis collections. The conjunction-form version of completeusersproof.cmd. It allows the User to avoid superflous virtual hypotheses. This proof was completed automatically by a tools program which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. suctrALTcf 45613 is suctrALTcfVD 45614 without virtual deductions and was derived automatically from suctrALTcfVD 45614. The version of completeusersproof.cmd used is capable of only generating conjunction-form unification theorems, not unification deductions. (Contributed by Alan Sare, 13-Jun-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

1::	⊢ (   Tr 𝐴   ▶   Tr 𝐴   )
2::	⊢ (   ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   )
3:2:	⊢ (   ......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑧 ∈ 𝑦   )
4::	⊢ (   ................................... ....... 𝑦 ∈ 𝐴   ▶   𝑦 ∈ 𝐴   )
5:1,3,4:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ 𝐴   )
6::	⊢ 𝐴 ⊆ suc 𝐴
7:5,6:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) , 𝑦 ∈ 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
8:7:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)    )   ▶   (𝑦 ∈ 𝐴 → 𝑧 ∈ suc 𝐴)   )
9::	⊢ (   ................................... ...... 𝑦 = 𝐴   ▶   𝑦 = 𝐴   )
10:3,9:	⊢ (   ........ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧 ∈ 𝐴   )
11:10,6:	⊢ (   ........ (   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴), 𝑦 = 𝐴   )   ▶   𝑧 ∈ suc 𝐴   )
12:11:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 = 𝐴 → 𝑧 ∈ suc 𝐴)   )
13:2:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   𝑦 ∈ suc 𝐴   )
14:13:	⊢ (   .......... (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)   ▶   (𝑦 ∈ 𝐴 ∨ 𝑦 = 𝐴)   )
15:8,12,14:	⊢ (   (   Tr 𝐴   ,   (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴)    )   ▶   𝑧 ∈ suc 𝐴   )
16:15:	⊢ (   Tr 𝐴   ▶   ((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
17:16:	⊢ (   Tr 𝐴   ▶   ∀𝑧∀𝑦((𝑧 ∈ 𝑦 ∧ 𝑦 ∈ suc 𝐴) → 𝑧 ∈ suc 𝐴)   )
18:17:	⊢ (   Tr 𝐴   ▶   Tr suc 𝐴   )
qed:18:	⊢ (Tr 𝐴 → Tr suc 𝐴)

⊢ (Tr 𝐴 → Tr suc 𝐴)

21.42.10  Theorems with a VD proof in conventional notation derived from a VD proof

Theorem

suctrALT3 45615

The successor of a transitive class is transitive. suctrALT3 45615 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/suctralt3vd.html 45615. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 45261 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 19 used jaoded 45258). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 24 used dftr2 5221) . (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (Tr 𝐴 → Tr suc 𝐴)

Theorem

sspwimpALT 45616

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. sspwimpALT 45616 is the completed proof in conventional notation of the Virtual Deduction proof https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html 45616. It was completed manually. The potential for automated derivation from the VD proof exists. See wvd1 45261 for a description of Virtual Deduction. Some sub-theorems of the proof were completed using a unification deduction (e.g., the sub-theorem whose assertion is step 9 used elpwgded 45256). Unification deductions employ Mario Carneiro's metavariable concept. Some sub-theorems were completed using a unification theorem (e.g., the sub-theorem whose assertion is step 5 used elpwi 4570). (Contributed by Alan Sare, 3-Dec-2015.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

unisnALT 45617

A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. The User manually input on a mmj2 Proof Worksheet, without labels, all steps of unisnALT 45617 except 1, 11, 15, 21, and 30. With execution of the mmj2 unification command, mmj2 could find labels for all steps except for 2, 12, 16, 22, and 31 (and the then non-existing steps 1, 11, 15, 21, and 30). mmj2 could not find reference theorems for those five steps because the hypothesis field of each of these steps was empty and none of those steps unifies with a theorem in set.mm. Each of these five steps is a semantic variation of a theorem in set.mm and is 2-step provable. mmj2 does not have the ability to automatically generate the semantic variation in set.mm of a theorem in a mmj2 Proof Worksheet unless the theorem in the Proof Worksheet is labeled with a 1-hypothesis deduction whose hypothesis is a theorem in set.mm which unifies with the theorem in the Proof Worksheet. The stepprover.c program, which invokes mmj2, has this capability. stepprover.c automatically generated steps 1, 11, 15, 21, and 30, labeled all steps, and generated the RPN proof of unisnALT 45617. Roughly speaking, stepprover.c added to the Proof Worksheet a labeled duplicate step of each non-unifying theorem for each label in a text file, labels.txt, containing a list of labels provided by the User. Upon mmj2 unification, stepprover.c identified a label for each of the five theorems which 2-step proves it. For unisnALT 45617, the label list is a list of all 1-hypothesis propositional calculus deductions in set.mm. stepproverp.c is the same as stepprover.c except that it intermittently pauses during execution, allowing the User to observe the changes to a text file caused by the execution of particular statements of the program. (Contributed by Alan Sare, 19-Aug-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐴 ∈ V    ⇒   ⊢ ∪ {𝐴} = 𝐴

21.42.11  Theorems with a proof in conventional notation derived from a VD proof

Theorems with a proof in conventional notation automatically derived by completeusersproof.c from a Virtual Deduction User's Proof.

Theorem

notnotrALT2 45618

Converse of double negation. Theorem *2.14 of [WhiteheadRussell] p. 102. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ¬ 𝜑 → 𝜑)

Theorem

sspwimpALT2 45619

If a class is a subclass of another class, then its power class is a subclass of that other class's power class. Left-to-right implication of Exercise 18 of [TakeutiZaring] p. 18. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in https://us.metamath.org/other/completeusersproof/sspwimpaltvd.html. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ⊆ 𝐵 → 𝒫 𝐴 ⊆ 𝒫 𝐵)

Theorem

e2ebindALT 45620

Absorption of an existential quantifier of a double existential quantifier of non-distinct variables. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in e2ebindVD 45603. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑦𝜑 ↔ ∃𝑦𝜑))

Theorem

ax6e2ndALT 45621*

If at least two sets exist (dtru 5420), then the same is true expressed in an alternate form similar to the form of ax6e 2415. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD 45599. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

ax6e2ndeqALT 45622*

"At least two sets exist" expressed in the form of dtru 5420 is logically equivalent to the same expressed in a form similar to ax6e 2415 if dtru 5420 is false implies 𝑢 = 𝑣. Proof derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndeqVD 45600. (Contributed by Alan Sare, 11-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) ↔ ∃𝑥∃𝑦(𝑥 = 𝑢 ∧ 𝑦 = 𝑣))

Theorem

2sb5ndALT 45623*

Equivalence for double substitution 2sb5 2313 without distinct 𝑥, 𝑦 requirement. 2sb5nd 45252 is derived from 2sb5ndVD 45601. The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD 45601. (Contributed by Alan Sare, 19-Sep-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((¬ ∀𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣) → ([𝑢 / 𝑥][𝑣 / 𝑦]𝜑 ↔ ∃𝑥∃𝑦((𝑥 = 𝑢 ∧ 𝑦 = 𝑣) ∧ 𝜑)))

Theorem

chordthmALT 45624*

The intersecting chords theorem. If points A, B, C, and D lie on a circle (with center Q, say), and the point P is on the interior of the segments AB and CD, then the two products of lengths PA · PB and PC · PD are equal. The Euclidean plane is identified with the complex plane, and the fact that P is on AB and on CD is expressed by the hypothesis that the angles APB and CPD are equal to π. The result is proven by using chordthmlem5 26982 twice to show that PA · PB and PC · PD both equal BQ ² − PQ ² . This is similar to the proof of the theorem given in Euclid's Elements, where it is Proposition III.35. Proven by David Moews on 28-Feb-2017 as chordthm 26983. https://us.metamath.org/other/completeusersproof/chordthmaltvd.html 26983 is a Virtual Deduction User's Proof transcription of chordthm 26983. That VD User's Proof was input into completeusersproof, automatically generating this chordthmALT 45624 Metamath proof. (Contributed by Alan Sare, 19-Sep-2017.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ 𝐹 = (𝑥 ∈ (ℂ ∖ {0}), 𝑦 ∈ (ℂ ∖ {0}) ↦ (ℑ‘(log‘(𝑦 / 𝑥))))    &   ⊢ (𝜑 → 𝐴 ∈ ℂ)    &   ⊢ (𝜑 → 𝐵 ∈ ℂ)    &   ⊢ (𝜑 → 𝐶 ∈ ℂ)    &   ⊢ (𝜑 → 𝐷 ∈ ℂ)    &   ⊢ (𝜑 → 𝑃 ∈ ℂ)    &   ⊢ (𝜑 → 𝐴 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐵 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐶 ≠ 𝑃)    &   ⊢ (𝜑 → 𝐷 ≠ 𝑃)    &   ⊢ (𝜑 → ((𝐴 − 𝑃)𝐹(𝐵 − 𝑃)) = π)    &   ⊢ (𝜑 → ((𝐶 − 𝑃)𝐹(𝐷 − 𝑃)) = π)    &   ⊢ (𝜑 → 𝑄 ∈ ℂ)    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐵 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐶 − 𝑄)))    &   ⊢ (𝜑 → (abs‘(𝐴 − 𝑄)) = (abs‘(𝐷 − 𝑄)))    ⇒   ⊢ (𝜑 → ((abs‘(𝑃 − 𝐴)) · (abs‘(𝑃 − 𝐵))) = ((abs‘(𝑃 − 𝐶)) · (abs‘(𝑃 − 𝐷))))

Theorem

isosctrlem1ALT 45625

Lemma for isosctr 26967. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 26967. As it is verified by the Metamath program, isosctrlem1ALT 45625 verifies https://us.metamath.org/other/completeusersproof/isosctrlem1altvd.html 45625. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ ((𝐴 ∈ ℂ ∧ (abs‘𝐴) = 1 ∧ ¬ 1 = 𝐴) → (ℑ‘(log‘(1 − 𝐴))) ≠ π)

Theorem

iunconnlem2 45626*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconlem2vd.html. As it is verified by the Metamath program, iunconnlem2 45626 verifies https://us.metamath.org/other/completeusersproof/iunconlem2vd.html 45626. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜓 ↔ ((((((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑣 ∈ 𝐽) ∧ (𝑢 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑣 ∩ ∪ 𝑘 ∈ 𝐴 𝐵) ≠ ∅) ∧ (𝑢 ∩ 𝑣) ⊆ (𝑋 ∖ ∪ 𝑘 ∈ 𝐴 𝐵)) ∧ ∪ 𝑘 ∈ 𝐴 𝐵 ⊆ (𝑢 ∪ 𝑣)))    &   ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

iunconnALT 45627*

The indexed union of connected overlapping subspaces sharing a common point is connected. This proof was automatically derived by completeusersproof from its Virtual Deduction proof counterpart https://us.metamath.org/other/completeusersproof/iunconaltvd.html. As it is verified by the Metamath program, iunconnALT 45627 verifies https://us.metamath.org/other/completeusersproof/iunconaltvd.html 45627. (Contributed by Alan Sare, 22-Apr-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋))    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ⊆ 𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝑃 ∈ 𝐵)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → (𝐽 ↾_t 𝐵) ∈ Conn)    ⇒   ⊢ (𝜑 → (𝐽 ↾_t ∪ 𝑘 ∈ 𝐴 𝐵) ∈ Conn)

Theorem

sineq0ALT 45628

A complex number whose sine is zero is an integer multiple of π. The Virtual Deduction form of the proof is https://us.metamath.org/other/completeusersproof/sineq0altvd.html. The Metamath form of the proof is sineq0ALT 45628. The Virtual Deduction proof is based on Mario Carneiro's revision of Norm Megill's proof of sineq0 26670. The Virtual Deduction proof is verified by automatically transforming it into the Metamath form of the proof using completeusersproof, which is verified by the Metamath program. The proof of https://us.metamath.org/other/completeusersproof/sineq0altro.html 26670 is a form of the completed proof which preserves the Virtual Deduction proof's step numbers and their ordering. (Contributed by Alan Sare, 13-Jun-2018.) (Proof modification is discouraged.) (New usage is discouraged.)

⊢ (𝐴 ∈ ℂ → ((sin‘𝐴) = 0 ↔ (𝐴 / π) ∈ ℤ))

21.43  Mathbox for Eric Schmidt

21.43.1  Miscellany

Theorem

rspesbcd 45629*

Restricted quantifier version of spesbcd 3837. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜑 → 𝐴 ∈ 𝐵)    &   ⊢ (𝜑 → [𝐴 / 𝑥]𝜓)    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝐵 𝜓)

Theorem

rext0 45630*

Nonempty existential quantification of a theorem is true. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝜑    ⇒   ⊢ (∃𝑥 ∈ 𝐴 𝜑 ↔ 𝐴 ≠ ∅)

21.43.2  Study of dfbi1ALT

Theorem

dfbi1ALTa 45631

Version of dfbi1ALT 217 using ⊤ for step 2 and shortened using a1i 11, a2i 15, and con4i 115. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

Theorem

simprimi 45632

Inference associated with simprim 167. Proved exactly as step 11 is obtained from step 4 in dfbi1ALTa 45631. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ¬ (𝜑 → ¬ 𝜓)    ⇒   ⊢ 𝜓

Theorem

dfbi1ALTb 45633

Further shorten dfbi1ALTa 45631 using simprimi 45632. (Contributed by Eric Schmidt, 22-Oct-2025.) (New usage is discouraged.) (Proof modification is discouraged.)

⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))

21.43.3  Relation-preserving functions

Syntax

wrelp 45634

Extend the definition of a wff to include the relation-preserving property. (Contributed by Eric Schmidt, 11-Oct-2025.)

wff 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Definition

df-relp 45635*

Define the relation-preserving predicate. This is a viable notion of "homomorphism" corresponding to df-isom 6547. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ (𝐻:𝐴⟶𝐵 ∧ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥𝑅𝑦 → (𝐻‘𝑥)𝑆(𝐻‘𝑦))))

Theorem

relpeq1 45636

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 = 𝐺 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐺 RelPres 𝑅, 𝑆(𝐴, 𝐵)))

Theorem

relpeq2 45637

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑅 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑇, 𝑆(𝐴, 𝐵)))

Theorem

relpeq3 45638

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝑆 = 𝑇 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑇(𝐴, 𝐵)))

Theorem

relpeq4 45639

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐴 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐶, 𝐵)))

Theorem

relpeq5 45640

Equality theorem for relation-preserving functions. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐵 = 𝐶 → (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ↔ 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐶)))

Theorem

nfrelp 45641

Bound-variable hypothesis builder for a relation-preserving function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ Ⅎ𝑥𝐻    &   ⊢ Ⅎ𝑥𝑅    &   ⊢ Ⅎ𝑥𝑆    &   ⊢ Ⅎ𝑥𝐴    &   ⊢ Ⅎ𝑥𝐵    ⇒   ⊢ Ⅎ𝑥 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵)

Theorem

relpf 45642

A relation-preserving function is a function. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → 𝐻:𝐴⟶𝐵)

Theorem

relprel 45643

A relation-preserving function preserves the relation. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (𝐶𝑅𝐷 → (𝐻‘𝐶)𝑆(𝐻‘𝐷)))

Theorem

relpmin 45644

A preimage of a minimal element under a relation-preserving function is minimal. Essentially one half of isomin 7337. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ ((𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) ∧ (𝐶 ⊆ 𝐴 ∧ 𝐷 ∈ 𝐴)) → (((𝐻 “ 𝐶) ∩ (^◡𝑆 “ {(𝐻‘𝐷)})) = ∅ → (𝐶 ∩ (^◡𝑅 “ {𝐷})) = ∅))

Theorem

relpfrlem 45645*

Lemma for relpfr 45646. Proved without using the Axiom of Replacement. This is isofrlem 7340 with weaker hypotheses. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝜑 → 𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵))    &   ⊢ (𝜑 → (𝐻 “ 𝑥) ∈ V)    ⇒   ⊢ (𝜑 → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

Theorem

relpfr 45646

If the image of a set under a relation-preserving function is well-founded, so is the set. See isofr 7342 for a bidirectional statement. A more general version of Lemma I.9.9 of [Kunen2] p. 47. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ (𝐻 RelPres 𝑅, 𝑆(𝐴, 𝐵) → (𝑆 Fr 𝐵 → 𝑅 Fr 𝐴))

21.43.4  Orbits

Theorem

orbitex 45647

Orbits exist. Given a set 𝐴 and a function 𝐹, the orbit of 𝐴 under 𝐹 is the smallest set 𝑍 such that 𝐴 ∈ 𝑍 and 𝑍 is closed under 𝐹. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (rec(𝐹, 𝐴) “ ω) ∈ V

Theorem

orbitinit 45648

A set is contained in its orbit. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitcl 45649

The orbit under a function is closed under the function. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ (𝐵 ∈ (rec(𝐹, 𝐴) “ ω) → (𝐹‘𝐵) ∈ (rec(𝐹, 𝐴) “ ω))

Theorem

orbitclmpt 45650

Version of orbitcl 45649 using maps-to notation. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ Ⅎ𝑥𝐵    &   ⊢ Ⅎ𝑥𝐷    &   ⊢ 𝑍 = (rec((𝑥 ∈ V ↦ 𝐶), 𝐴) “ ω)    &   ⊢ (𝑥 = 𝐵 → 𝐶 = 𝐷)    ⇒   ⊢ ((𝐵 ∈ 𝑍 ∧ 𝐷 ∈ 𝑉) → 𝐷 ∈ 𝑍)

21.43.5  Well-founded sets

Theorem

trwf 45651

The class of well-founded sets is transitive. (Contributed by Eric Schmidt, 9-Sep-2025.)

⊢ Tr ∪ (𝑅₁ “ On)

Theorem

rankrelp 45652

The rank function preserves ∈. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ rank RelPres E , E (∪ (𝑅₁ “ On), On)

Theorem

wffr 45653

The class of well-founded sets is well-founded. Lemma I.9.24(2) of [Kunen2] p. 53. (Contributed by Eric Schmidt, 11-Oct-2025.)

⊢ E Fr ∪ (𝑅₁ “ On)

Theorem

trfr 45654

A transitive class well-founded by ∈ is a subclass of the class of well-founded sets. Part of Lemma I.9.21 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ ((Tr 𝐴 ∧ E Fr 𝐴) → 𝐴 ⊆ ∪ (𝑅₁ “ On))

Theorem

tcfr 45655

A set is well-founded if and only if its transitive closure is well-founded by ∈. This characterization of well-founded sets is that in Definition I.9.20 of [Kunen2] p. 53. (Contributed by Eric Schmidt, 26-Oct-2025.)

⊢ 𝐴 ∈ V    ⇒   ⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) ↔ E Fr (TC‘𝐴))

Theorem

xpwf 45656

The Cartesian product of two well-founded sets is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ ((𝐴 ∈ ∪ (𝑅₁ “ On) ∧ 𝐵 ∈ ∪ (𝑅₁ “ On)) → (𝐴 × 𝐵) ∈ ∪ (𝑅₁ “ On))

Theorem

dmwf 45657

The domain of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → dom 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

rnwf 45658

The range of a well-founded set is well-founded. (Contributed by Eric Schmidt, 12-Sep-2025.)

⊢ (𝐴 ∈ ∪ (𝑅₁ “ On) → ran 𝐴 ∈ ∪ (𝑅₁ “ On))

Theorem

relwf 45659

A relation is a well-founded set iff its domain and range are. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (Rel 𝑅 → (𝑅 ∈ ∪ (𝑅₁ “ On) ↔ (dom 𝑅 ∈ ∪ (𝑅₁ “ On) ∧ ran 𝑅 ∈ ∪ (𝑅₁ “ On))))

21.43.6  Absoluteness in transitive models

Theorem

ralabso 45660*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∀𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜑)))

Theorem

rexabso 45661*

Simplification of restricted quantification in a transitive class. When 𝜑 is quantifier-free, this shows that the formula ∃𝑥 ∈ 𝑦𝜑 is absolute for transitive models, which is a particular case of Lemma I.16.2 of [Kunen2] p. 95. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜑 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜑)))

Theorem

ralabsod 45662*

Deduction form of ralabso 45660. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜓)))

Theorem

rexabsod 45663*

Deduction form of rexabso 45661. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜓)))

Theorem

ralabsobidv 45664*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∀𝑥 ∈ 𝐴 𝜓 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝜒)))

Theorem

rexabsobidv 45665*

Formula-building lemma for proving absoluteness results. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝜑 → Tr 𝑀)    &   ⊢ (𝜑 → (𝜓 ↔ 𝜒))    ⇒   ⊢ ((𝜑 ∧ 𝐴 ∈ 𝑀) → (∃𝑥 ∈ 𝐴 𝜓 ↔ ∃𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 ∧ 𝜒)))

Theorem

ssabso 45666*

The notion "𝑥 is a subset of 𝑦 " is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ⊆ 𝐵 ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵)))

Theorem

disjabso 45667*

Disjointness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → ((𝐴 ∩ 𝐵) = ∅ ↔ ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝐴 → ¬ 𝑥 ∈ 𝐵)))

Theorem

n0abso 45668*

Nonemptiness is absolute for transitive models. Compare Example I.16.3 of [Kunen2] p. 96 and the following discussion. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ 𝐴 ∈ 𝑀) → (𝐴 ≠ ∅ ↔ ∃𝑥 ∈ 𝑀 𝑥 ∈ 𝐴))

21.43.7  Lemmas for showing axioms hold in models

Theorem

traxext 45669*

A transitive class models the Axiom of Extensionality ax-ext 2735. Lemma II.2.4(1) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 11-Sep-2025.)

⊢ (Tr 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 (∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦))

Theorem

modelaxreplem1 45670*

Lemma for modelaxrep 45673. We show that 𝑀 is closed under taking subsets. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ 𝐴 ⊆ 𝑥    ⇒   ⊢ (𝜓 → 𝐴 ∈ 𝑀)

Theorem

modelaxreplem2 45671*

Lemma for modelaxrep 45673. We define a class 𝐹 and show that the antecedent of Replacement implies that 𝐹 is a function. We use Replacement (in the form of funex 7219) to show that 𝐹 exists. Then we show that, under our hypotheses, the range of 𝐹 is a member of 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ran 𝐹 ∈ 𝑀)

Theorem

modelaxreplem3 45672*

Lemma for modelaxrep 45673. We show that the consequent of Replacement is satisfied with ran 𝐹 as the value of 𝑦. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → 𝑥 ⊆ 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    &   ⊢ (𝜓 → 𝑥 ∈ 𝑀)    &   ⊢ Ⅎ𝑤𝜓    &   ⊢ Ⅎ𝑧𝜓    &   ⊢ Ⅎ𝑧𝐹    &   ⊢ 𝐹 = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}    &   ⊢ (𝜓 → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))    ⇒   ⊢ (𝜓 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))

Theorem

modelaxrep 45673*

Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5239. Similar to Lemma II.2.4(6) of [Kunen2] p. 111. The first two hypotheses are those in Kunen. The reason for the third hypothesis that our version of Replacement is different from Kunen's (which is zfrep6 5251). If we assumed Regularity, we could eliminate this extra hypothesis, since under Regularity, the empty set is a member of every non-empty transitive class.

Note that, to obtain the relativization of an instance of Replacement to 𝑀, the formula ∀𝑦𝜑 would need to be replaced with ∀𝑦 ∈ 𝑀𝜒, where 𝜒 is 𝜑 with all quantifiers relativized to 𝑀. However, we can obtain this by using 𝑦 ∈ 𝑀 ∧ 𝜒 for 𝜑 in this theorem, so it does establish that all instances of Replacement hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (𝜓 → Tr 𝑀)    &   ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))    &   ⊢ (𝜓 → ∅ ∈ 𝑀)    ⇒   ⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))

Theorem

ssclaxsep 45674*

A class that is closed under subsets models the Axiom of Separation ax-sep 5258. Lemma II.2.4(3) of [Kunen2] p. 111.

Note that, to obtain the relativization of an instance of Separation to 𝑀, the formula 𝜑 would need to be replaced with its relativization to 𝑀. However, this new formula is a valid substitution for 𝜑, so this theorem does establish that all instances of Separation hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (∀𝑧 ∈ 𝑀 𝒫 𝑧 ⊆ 𝑀 → ∀𝑧 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑥 ∈ 𝑀 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑)))

Theorem

0elaxnul 45675*

A class that contains the empty set models the Null Set Axiom ax-nul 5270. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (∅ ∈ 𝑀 → ∃𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ¬ 𝑦 ∈ 𝑥)

Theorem

pwclaxpow 45676*

Suppose 𝑀 is a transitive class that is closed under power sets intersected with 𝑀. Then, 𝑀 models the Axiom of Power Sets ax-pow 5338. One direction of Lemma II.2.8 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ ∀𝑥 ∈ 𝑀 (𝒫 𝑥 ∩ 𝑀) ∈ 𝑀) → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Theorem

prclaxpr 45677*

A class that is closed under the pairing operation models the Axiom of Pairing ax-pr 5406. Lemma II.2.4(4) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ (∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 {𝑥, 𝑦} ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∀𝑦 ∈ 𝑀 ∃𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧))

Theorem

uniclaxun 45678*

A class that is closed under the union operation models the Axiom of Union ax-un 7734. Lemma II.2.4(5) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 1-Oct-2025.)

⊢ (∀𝑥 ∈ 𝑀 ∪ 𝑥 ∈ 𝑀 → ∀𝑥 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∃𝑤 ∈ 𝑀 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦))

Theorem

sswfaxreg 45679*

A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg 9555. Lemma II.2.4(2) of [Kunen2] p. 111. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (𝑀 ⊆ ∪ (𝑅₁ “ On) → ∀𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥))))

Theorem

omssaxinf2 45680*

A class that contains all ordinals up to and including ω models the Axiom of Infinity ax-inf2 9611. The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9608. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((ω ⊆ 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Theorem

omelaxinf2 45681*

A transitive class that contains ω models the Axiom of Infinity ax-inf2 9611. Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Infinity uses the defined notions ∅ and suc, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears.

The antecedent of this theorem is not enough to guarantee that the class models the alternate axiom ax-inf 9608. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((Tr 𝑀 ∧ ω ∈ 𝑀) → ∃𝑥 ∈ 𝑀 (∃𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑀 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑀 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦))))))

Theorem

dfac5prim 45682*

dfac5 10113 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (CHOICE ↔ ∀𝑥((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤))))

Theorem

ac8prim 45683*

ac8 10477 expanded into primitives. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ ((∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤 𝑤 ∈ 𝑧) ∧ ∀𝑧∀𝑤((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦(𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦∀𝑧(𝑧 ∈ 𝑥 → ∃𝑤∀𝑣((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

Theorem

modelac8prim 45684*

If 𝑀 is a transitive class, then the following are equivalent. (1) Every nonempty set 𝑥 ∈ 𝑀 of pairwise disjoint nonempty sets has a choice set in 𝑀. (2) The class 𝑀 models the Axiom of Choice, in the form ac8prim 45683.

Lemma II.2.11(7) of [Kunen2] p. 114. Kunen has the additional hypotheses that the Extensionality, Separation, Pairing, and Union axioms are true in 𝑀. This, apparently, is because Kunen's statement of the Axiom of Choice uses defined notions, including ∅ and ∩, and these axioms guarantee that these notions are well-defined. When we state the axiom using primitives only, the need for these hypotheses disappears. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ (Tr 𝑀 → (∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑥 𝑧 ≠ ∅ ∧ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑥 (𝑧 ≠ 𝑤 → (𝑧 ∩ 𝑤) = ∅)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑥 ∃!𝑣 𝑣 ∈ (𝑧 ∩ 𝑦)) ↔ ∀𝑥 ∈ 𝑀 ((∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑀 ∀𝑤 ∈ 𝑀 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑀 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑀 ∀𝑣 ∈ 𝑀 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))))

21.43.8  The class of well-founded sets is a model for ZFC

Theorem

wfaxext 45685*

The class of well-founded sets models the Axiom of Extensionality ax-ext 2735. Part of Corollary II.2.5 of [Kunen2] p. 112.

This is the first of a series of theorems showing that all the axioms of ZFC hold in the class of well-founded sets, which we here denote by 𝑊. More precisely, for each axiom of ZFC, we obtain a provable statement if we restrict all quantifiers to 𝑊 (including implicit universal quantifiers on free variables).

None of these proofs use the Axiom of Regularity. In particular, the Axiom of Regularity itself is proved to hold in 𝑊 without using Regularity. Further, the Axiom of Choice is used only in the proof that Choice holds in 𝑊. This has the consequence that any theorem of ZF (possibly proved using Regularity) can be proved, without using Regularity, to hold in 𝑊. This gives us a relative consistency result: If ZF without Regularity is consistent, so is ZF itself. Similarly, if ZFC without Regularity is consistent, so is ZFC itself. These consistency results are metatheorems and are part of Theorem II.2.13 of [Kunen2] p. 114.

(Contributed by Eric Schmidt, 11-Sep-2025.) (Revised by Eric Schmidt, 29-Sep-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 (∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ↔ 𝑧 ∈ 𝑦) → 𝑥 = 𝑦)

Theorem

wfaxrep 45686*

The class of well-founded sets models the Axiom of Replacement ax-rep 5239. Actually, our statement is stronger, since it is an instance of Replacement only when all quantifiers in ∀𝑦𝜑 are relativized to 𝑊. Essentially part of Corollary II.2.5 of [Kunen2] p. 112, but note that our Replacement is different from Kunen's. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∀𝑤 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑊 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))

Theorem

wfaxsep 45687*

The class of well-founded sets models the Axiom of Separation ax-sep 5258. Actually, our statement is stronger, since it is an instance of Separation only when all quantifiers in 𝜑 are relativized to 𝑊. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑧 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑥 ∈ 𝑊 (𝑥 ∈ 𝑦 ↔ (𝑥 ∈ 𝑧 ∧ 𝜑))

Theorem

wfaxnul 45688*

The class of well-founded sets models the Null Set Axiom ax-nul 5270. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ¬ 𝑦 ∈ 𝑥

Theorem

wfaxpow 45689*

The class of well-founded sets models the Axioms of Power Sets. Part of Corollary II.2.9 of [Kunen2] p. 113. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 → 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Theorem

wfaxpr 45690*

The class of well-founded sets models the Axiom of Pairing ax-pr 5406. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 29-Sep-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∀𝑦 ∈ 𝑊 ∃𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑤 = 𝑥 ∨ 𝑤 = 𝑦) → 𝑤 ∈ 𝑧)

Theorem

wfaxun 45691*

The class of well-founded sets models the Axiom of Union ax-un 7734. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (∃𝑤 ∈ 𝑊 (𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑥) → 𝑧 ∈ 𝑦)

Theorem

wfaxreg 45692*

The class of well-founded sets models the Axiom of Regularity ax-reg 9555. Part of Corollary II.2.5 of [Kunen2] p. 112. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 𝑦 ∈ 𝑥 → ∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑦 → ¬ 𝑧 ∈ 𝑥)))

Theorem

wfaxinf2 45693*

The class of well-founded sets models the Axiom of Infinity ax-inf2 9611. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∃𝑥 ∈ 𝑊 (∃𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 ∧ ∀𝑧 ∈ 𝑊 ¬ 𝑧 ∈ 𝑦) ∧ ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑥 → ∃𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 ∧ ∀𝑤 ∈ 𝑊 (𝑤 ∈ 𝑧 ↔ (𝑤 ∈ 𝑦 ∨ 𝑤 = 𝑦)))))

Theorem

wfac8prim 45694*

The class of well-founded sets 𝑊 models the Axiom of Choice. Since the previous theorems show that all the ZF axioms hold in 𝑊, we may use any statement that ZF proves is equivalent to Choice to prove this. We use ac8prim 45683. Part of Corollary II.2.12 of [Kunen2] p. 114. (Contributed by Eric Schmidt, 19-Oct-2025.)

⊢ 𝑊 = ∪ (𝑅₁ “ On)    ⇒   ⊢ ∀𝑥 ∈ 𝑊 ((∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 𝑤 ∈ 𝑧) ∧ ∀𝑧 ∈ 𝑊 ∀𝑤 ∈ 𝑊 ((𝑧 ∈ 𝑥 ∧ 𝑤 ∈ 𝑥) → (¬ 𝑧 = 𝑤 → ∀𝑦 ∈ 𝑊 (𝑦 ∈ 𝑧 → ¬ 𝑦 ∈ 𝑤)))) → ∃𝑦 ∈ 𝑊 ∀𝑧 ∈ 𝑊 (𝑧 ∈ 𝑥 → ∃𝑤 ∈ 𝑊 ∀𝑣 ∈ 𝑊 ((𝑣 ∈ 𝑧 ∧ 𝑣 ∈ 𝑦) ↔ 𝑣 = 𝑤)))

21.43.9  Permutation models

Theorem

brpermmodel 45695

The membership relation in a permutation model. We use a permutation 𝐹 of the universe to define a relation 𝑅 that serves as the membership relation in our model. The conclusion of this theorem is Definition II.9.1 of [Kunen2] p. 148. All the axioms of ZFC except for Regularity hold in permutation models, and Regularity will be false if 𝐹 is chosen appropriately. Thus, permutation models can be used to show that Regularity does not follow from the other axioms (with the usual proviso that the axioms are consistent). (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅𝐵 ↔ 𝐴 ∈ (𝐹‘𝐵))

Theorem

brpermmodelcnv 45696

Ordinary membership expressed in terms of the permutation model's membership relation. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    &   ⊢ 𝐴 ∈ V    &   ⊢ 𝐵 ∈ V    ⇒   ⊢ (𝐴𝑅(^◡𝐹‘𝐵) ↔ 𝐴 ∈ 𝐵)

Theorem

permaxext 45697*

The Axiom of Extensionality ax-ext 2735 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑧(𝑧𝑅𝑥 ↔ 𝑧𝑅𝑦) → 𝑥 = 𝑦)

Theorem

permaxrep 45698*

The Axiom of Replacement ax-rep 5239 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148.

Note that, to prove that an instance of Replacement holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Replacement holds. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    ⇒   ⊢ (∀𝑤∃𝑦∀𝑧(∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦∀𝑧(𝑧𝑅𝑦 ↔ ∃𝑤(𝑤𝑅𝑥 ∧ ∀𝑦𝜑)))

Theorem

permaxsep 45699*

The Axiom of Separation ax-sep 5258 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148.

Note that, to prove that an instance of Separation holds in the model, 𝜑 would need have all instances of ∈ replaced with 𝑅. But this still results in an instance of this theorem, so we do establish that Separation holds. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑦∀𝑥(𝑥𝑅𝑦 ↔ (𝑥𝑅𝑧 ∧ 𝜑))

Theorem

permaxnul 45700*

The Null Set Axiom ax-nul 5270 holds in permutation models. Part of Exercise II.9.2 of [Kunen2] p. 148. (Contributed by Eric Schmidt, 6-Nov-2025.)

⊢ 𝐹:V–1-1-onto→V    &   ⊢ 𝑅 = (^◡𝐹 ∘ E )    ⇒   ⊢ ∃𝑥∀𝑦 ¬ 𝑦𝑅𝑥