Metamath Proof Explorer

Theorem pgindnf

Description: Version of pgind with extraneous not-free requirements. (Contributed by Emmett Weisz, 27-May-2024) (New usage is discouraged.)

Ref Expression
Hypotheses pgindnf.1 ⊢ Ⅎ 𝑥 𝜑
pgindnf.2 ⊢ Ⅎ 𝑦 𝜑
pgindnf.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
pgindnf.4 ⊢ ( 𝑦 = 𝐴 → ( 𝜒 ↔ 𝜃 ) )
pgindnf.5 ⊢ ( 𝜑 → ∀ 𝑥 ( ∀ 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) 𝜒 → 𝜓 ) )
Assertion pgindnf ( 𝜑 → ( 𝐴 ∈ Pg → 𝜃 ) )

Proof

Step Hyp Ref Expression
1 pgindnf.1 ⊢ Ⅎ 𝑥 𝜑
2 pgindnf.2 ⊢ Ⅎ 𝑦 𝜑
3 pgindnf.3 ⊢ ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) )
4 pgindnf.4 ⊢ ( 𝑦 = 𝐴 → ( 𝜒 ↔ 𝜃 ) )
5 pgindnf.5 ⊢ ( 𝜑 → ∀ 𝑥 ( ∀ 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) 𝜒 → 𝜓 ) )
6 df-pg ⊢ Pg = setrecs ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) )
7 nfv ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ 𝑧 𝜒
8 1 7 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 𝜒 )
9 pgindlem ⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) ⊆ 𝑧 )
10 9 sseld ⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) → 𝑦 ∈ 𝑧 ) )
11 10 imim1d ⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( ( 𝑦 ∈ 𝑧 → 𝜒 ) → ( 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) → 𝜒 ) ) )
12 11 ralimdv2 ⊢ ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → ( ∀ 𝑦 ∈ 𝑧 𝜒 → ∀ 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) 𝜒 ) )
13 5 19.21bi ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( ( 1st ‘ 𝑥 ) ∪ ( 2nd ‘ 𝑥 ) ) 𝜒 → 𝜓 ) )
14 12 13 sylan9r ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) ) → ( ∀ 𝑦 ∈ 𝑧 𝜒 → 𝜓 ) )
15 14 impancom ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 𝜒 ) → ( 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) → 𝜓 ) )
16 8 15 ralrimi ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 𝜒 ) → ∀ 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) 𝜓 )
17 vex ⊢ 𝑧 ∈ V
18 pweq ⊢ ( 𝑎 = 𝑧 → 𝒫 𝑎 = 𝒫 𝑧 )
19 18 sqxpeqd ⊢ ( 𝑎 = 𝑧 → ( 𝒫 𝑎 × 𝒫 𝑎 ) = ( 𝒫 𝑧 × 𝒫 𝑧 ) )
20 eqid ⊢ ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) = ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) )
21 vpwex ⊢ 𝒫 𝑧 ∈ V
22 21 21 xpex ⊢ ( 𝒫 𝑧 × 𝒫 𝑧 ) ∈ V
23 19 20 22 fvmpt ⊢ ( 𝑧 ∈ V → ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) = ( 𝒫 𝑧 × 𝒫 𝑧 ) )
24 17 23 ax-mp ⊢ ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) = ( 𝒫 𝑧 × 𝒫 𝑧 )
25 24 eqcomi ⊢ ( 𝒫 𝑧 × 𝒫 𝑧 ) = ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 )
26 25 a1i ⊢ ( 𝑥 = 𝑦 → ( 𝒫 𝑧 × 𝒫 𝑧 ) = ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) )
27 3 26 cbvralv2 ⊢ ( ∀ 𝑥 ∈ ( 𝒫 𝑧 × 𝒫 𝑧 ) 𝜓 ↔ ∀ 𝑦 ∈ ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) 𝜒 )
28 16 27 sylib ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝑧 𝜒 ) → ∀ 𝑦 ∈ ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) 𝜒 )
29 28 ex ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑧 𝜒 → ∀ 𝑦 ∈ ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) 𝜒 ) )
30 29 alrimiv ⊢ ( 𝜑 → ∀ 𝑧 ( ∀ 𝑦 ∈ 𝑧 𝜒 → ∀ 𝑦 ∈ ( ( 𝑎 ∈ V ↦ ( 𝒫 𝑎 × 𝒫 𝑎 ) ) ‘ 𝑧 ) 𝜒 ) )
31 6 4 30 setis ⊢ ( 𝜑 → ( 𝐴 ∈ Pg → 𝜃 ) )